HepLean Documentation

Mathlib.Algebra.Group.Units.Opposite

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 (Units.opEquiv u)) = MulOpposite.unop ↑u
      source
      @[simp]
      theorem AddUnits.coe_unop_opEquiv {M : Type u_2} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :
      ↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u
      source
      @[simp]
      theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : Mˣᵐᵒᵖ) :
      ↑(Units.opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)
      source
      @[simp]
      theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :
      ↑(AddUnits.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