# Units in multiplicative and additive opposites #

source
def Units.opEquiv {M : Type u_2} [Monoid M] :
M ᵐᵒᵖ ˣ ≃* M ˣ ᵐᵒᵖ

The units of the opposites are equivalent to the opposites of the units.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def AddUnits.opEquiv {M : Type u_2} [AddMonoid M] :
AddUnits M ᵃᵒᵖ ≃+ (AddUnits M)ᵃᵒᵖ

The additive units of the additive opposites are equivalent to the additive opposites of the additive units.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Units.coe_unop_opEquiv {M : Type u_2} [Monoid M] (u : M ᵐᵒᵖ ˣ) :
↑(MulOpposite.unop (opEquiv u)) = MulOpposite.unop ↑u
source
@[simp]
theorem AddUnits.coe_unop_opEquiv {M : Type u_2} [AddMonoid M] (u : AddUnits M ᵃᵒᵖ) :
↑(AddOpposite.unop (opEquiv u)) = AddOpposite.unop ↑u
source
@[simp]
theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : M ˣ ᵐᵒᵖ) :
↑(opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)
source
@[simp]
theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :
↑(opEquiv.symm u) = AddOpposite.op ↑(AddOpposite.unop u)
source
theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) :
IsUnit (MulOpposite.op m)
source
theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) :
IsAddUnit (AddOpposite.op m)
source
theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : M ᵐᵒᵖ} (h : IsUnit m) :
IsUnit (MulOpposite.unop m)
source
theorem IsAddUnit.unop {M : Type u_2} [AddMonoid M] {m : M ᵃᵒᵖ} (h : IsAddUnit m) :
IsAddUnit (AddOpposite.unop m)
source
@[simp]
theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} :
IsUnit (MulOpposite.op m) ↔ IsUnit m
source
@[simp]
theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} :
IsAddUnit (AddOpposite.op m) ↔ IsAddUnit m
source
@[simp]
theorem isUnit_unop {M : Type u_2} [Monoid M] {m : M ᵐᵒᵖ} :
IsUnit (MulOpposite.unop m) ↔ IsUnit m
source
@[simp]
theorem isAddUnit_unop {M : Type u_2} [AddMonoid M] {m : M ᵃᵒᵖ} :
IsAddUnit (AddOpposite.unop m) ↔ IsAddUnit m