Multiplicative and additive equivalence acting on units. #
@[simp]
@[simp]
Left multiplication by a unit of a monoid is a permutation of the underlying type.
Equations
Instances For
Left addition of an additive unit is a permutation of the underlying type.
Equations
Instances For
@[simp]
@[simp]
theorem
Units.mulLeft_bijective
{M : Type u_3}
[Monoid M]
(a : Mˣ)
:
Function.Bijective fun (x : M) => ↑a * x
theorem
AddUnits.addLeft_bijective
{M : Type u_3}
[AddMonoid M]
(a : AddUnits M)
:
Function.Bijective fun (x : M) => ↑a + x
Right multiplication by a unit of a monoid is a permutation of the underlying type.
Equations
Instances For
Right addition of an additive unit is a permutation of the underlying type.
Equations
Instances For
@[simp]
@[simp]
theorem
Units.mulRight_bijective
{M : Type u_3}
[Monoid M]
(a : Mˣ)
:
Function.Bijective fun (x : M) => x * ↑a
theorem
AddUnits.addRight_bijective
{M : Type u_3}
[AddMonoid M]
(a : AddUnits M)
:
Function.Bijective fun (x : M) => x + ↑a
@[simp]
@[simp]
@[simp]
Extra simp lemma that dsimp
can use. simp
will never use this.
@[simp]
Extra simp lemma that dsimp
can use. simp
will never use this.
@[simp]
@[simp]
theorem
Group.mulLeft_bijective
{G : Type u_5}
[Group G]
(a : G)
:
Function.Bijective fun (x : G) => a * x
theorem
AddGroup.addLeft_bijective
{G : Type u_5}
[AddGroup G]
(a : G)
:
Function.Bijective fun (x : G) => a + x
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Extra simp lemma that dsimp
can use. simp
will never use this.
@[simp]
Extra simp lemma that dsimp
can use. simp
will never use this.
theorem
Group.mulRight_bijective
{G : Type u_5}
[Group G]
(a : G)
:
Function.Bijective fun (x : G) => x * a
theorem
AddGroup.addRight_bijective
{G : Type u_5}
[AddGroup G]
(a : G)
:
Function.Bijective fun (x : G) => x + a
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
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
Instances For
@[simp]
@[simp]
@[simp]
instance
isLocalHom_equiv
{F : Type u_1}
{M : Type u_3}
{N : Type u_4}
[Monoid M]
[Monoid N]
[EquivLike F M N]
[MulEquivClass F M N]
(f : F)
: