Multiplicative and additive equivalence acting on units. #
An additive group is isomorphic to its group of additive units
A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.
Equations
- Units.mapEquiv h = let __src := Units.map h.toMonoidHom; { toFun := (↑__src).toFun, invFun := ⇑(Units.map h.symm.toMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Left addition of an additive unit is a permutation of the underlying type.
Left multiplication by a unit of a monoid is a permutation of the underlying type.
Right addition of an additive unit is a permutation of the underlying type.
Right multiplication by a unit of a monoid is a permutation of the underlying type.
Left addition in an AddGroup
is a permutation of the underlying type.
Equations
- Equiv.addLeft a = (toAddUnits a).addLeft
Left multiplication in a Group
is a permutation of the underlying type.
Equations
- Equiv.mulLeft a = (toUnits a).mulLeft
Extra simp lemma that dsimp
can use. simp
will never use this.
Extra simp lemma that dsimp
can use. simp
will never use this.
Right addition in an AddGroup
is a permutation of the underlying type.
Equations
- Equiv.addRight a = (toAddUnits a).addRight
Right multiplication in a Group
is a permutation of the underlying type.
Equations
- Equiv.mulRight a = (toUnits a).mulRight
Extra simp lemma that dsimp
can use. simp
will never use this.
Extra simp lemma that dsimp
can use. simp
will never use this.
A version of Equiv.addLeft a (-b)
that is defeq to a - b
.
Equations
- Equiv.subLeft a = { toFun := fun (b : G) => a - b, invFun := fun (b : G) => -b + a, left_inv := ⋯, right_inv := ⋯ }
A version of Equiv.mulLeft a b⁻¹
that is defeq to a / b
.
Equations
- Equiv.divLeft a = { toFun := fun (b : G) => a / b, invFun := fun (b : G) => b⁻¹ * a, left_inv := ⋯, right_inv := ⋯ }
A version of Equiv.addRight (-a) b
that is defeq to b - a
.
Equations
- Equiv.subRight a = { toFun := fun (b : G) => b - a, invFun := fun (b : G) => b + a, left_inv := ⋯, right_inv := ⋯ }
A version of Equiv.mulRight a⁻¹ b
that is defeq to b / a
.
Equations
- Equiv.divRight a = { toFun := fun (b : G) => b / a, invFun := fun (b : G) => b * a, left_inv := ⋯, right_inv := ⋯ }
In a DivisionCommMonoid
, Equiv.inv
is a MulEquiv
. There is a variant of this
MulEquiv.inv' G : G ≃* Gᵐᵒᵖ
for the non-commutative case.
Equations
- MulEquiv.inv G = let __src := Equiv.inv G; { toFun := Inv.inv, invFun := Inv.inv, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }