Multiplicative and additive equivs #
In this file we define two extensions of Equiv
called AddEquiv
and MulEquiv
, which are
datatypes representing isomorphisms of AddMonoid
s/AddGroup
s and Monoid
s/Group
s.
Main definitions #
≃*
(MulEquiv
),≃+
(AddEquiv
): bundled equivalences that preserve multiplication/addition (and are therefore monoid and group isomorphisms).MulEquivClass
,AddEquivClass
: classes for types containing bundled equivalences that preserve multiplication/addition.
Notations #
The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.
Tags #
Equiv, MulEquiv, AddEquiv
AddEquiv α β
is the type of an equiv α ≃ β
which preserves addition.
- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
Instances For
MulEquiv α β
is the type of an equiv α ≃ β
which preserves multiplication.
- toFun : M → N
- invFun : N → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
Instances For
Alias of EmbeddingLike.map_eq_one_iff
.
Alias of EmbeddingLike.map_ne_one_iff
.
Turn an element of a type F
satisfying MulEquivClass F α β
into an actual
MulEquiv
. This is declared as the default coercion from F
to α ≃* β
.
Equations
Instances For
Turn an element of a type F
satisfying AddEquivClass F α β
into an actual
AddEquiv
. This is declared as the default coercion from F
to α ≃+ β
.
Equations
Instances For
Any type satisfying MulEquivClass
can be cast into MulEquiv
via
MulEquivClass.toMulEquiv
.
Equations
Any type satisfying AddEquivClass
can be cast into AddEquiv
via
AddEquivClass.toAddEquiv
.
Equations
simp
-normal form of toFun_eq_coe
.
The identity map is a multiplicative isomorphism.
Equations
Instances For
The identity map is an additive isomorphism.
Equations
Instances For
Monoids #
A multiplicative isomorphism of monoids sends 1
to 1
(and is hence a monoid isomorphism).
An additive isomorphism of additive monoids sends 0
to 0
(and is hence an additive monoid isomorphism).
A bijective Semigroup
homomorphism is an isomorphism
Equations
Instances For
A bijective AddSemigroup
homomorphism is an isomorphism
Equations
Instances For
Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.
Equations
Instances For
Extract the forward direction of an additive equivalence as an addition-preserving function.
Equations
Instances For
Groups #
A multiplicative equivalence of groups preserves inversion.
An additive equivalence of additive groups preserves negation.
A multiplicative equivalence of groups preserves division.
An additive equivalence of additive groups preserves subtractions.
Given a pair of multiplicative homomorphisms f
, g
such that g.comp f = id
and
f.comp g = id
, returns a multiplicative equivalence with toFun = f
and invFun = g
. This
constructor is useful if the underlying type(s) have specialized ext
lemmas for multiplicative
homomorphisms.
Equations
Instances For
Given a pair of additive homomorphisms f
, g
such that g.comp f = id
and
f.comp g = id
, returns an additive equivalence with toFun = f
and invFun = g
. This
constructor is useful if the underlying type(s) have specialized ext
lemmas for additive
homomorphisms.
Equations
Instances For
Given a pair of monoid homomorphisms f
, g
such that g.comp f = id
and f.comp g = id
,
returns a multiplicative equivalence with toFun = f
and invFun = g
. This constructor is
useful if the underlying type(s) have specialized ext
lemmas for monoid homomorphisms.
Equations
Instances For
Given a pair of additive monoid homomorphisms f
, g
such that g.comp f = id
and f.comp g = id
, returns an additive equivalence with toFun = f
and invFun = g
. This
constructor is useful if the underlying type(s) have specialized ext
lemmas for additive
monoid homomorphisms.