Documentation

Mathlib.Algebra.Group.Units.Opposite

Units in multiplicative and additive opposites #

source
๐Ÿ”ธ coverage
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
    Instances For
      source
      ๐Ÿ”ธ coverage
      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
        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Units.coe_unop_opEquiv {M : Type u_2} [Monoid M] (u : Mแตแต’แต–หฃ) :
          โ†‘(MulOpposite.unop (opEquiv u)) = MulOpposite.unop โ†‘u
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddUnits.coe_unop_opEquiv {M : Type u_2} [AddMonoid M] (u : AddUnits Mแตƒแต’แต–) :
          โ†‘(AddOpposite.unop (opEquiv u)) = AddOpposite.unop โ†‘u
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : Mหฃแตแต’แต–) :
          โ†‘(opEquiv.symm u) = MulOpposite.op โ†‘(MulOpposite.unop u)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)แตƒแต’แต–) :
          โ†‘(opEquiv.symm u) = AddOpposite.op โ†‘(AddOpposite.unop u)
          source
          ๐Ÿ“ coverage
          theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) :
          IsUnit (MulOpposite.op m)
          source
          ๐Ÿ“ coverage
          theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) :
          IsAddUnit (AddOpposite.op m)
          source
          ๐Ÿ“ coverage
          theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : Mแตแต’แต–} (h : IsUnit m) :
          IsUnit (MulOpposite.unop m)
          source
          ๐Ÿ“ coverage
          theorem IsAddUnit.unop {M : Type u_2} [AddMonoid M] {m : Mแตƒแต’แต–} (h : IsAddUnit m) :
          IsAddUnit (AddOpposite.unop m)
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} :
          IsUnit (MulOpposite.op m) โ†” IsUnit m
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} :
          IsAddUnit (AddOpposite.op m) โ†” IsAddUnit m
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem isUnit_unop {M : Type u_2} [Monoid M] {m : Mแตแต’แต–} :
          IsUnit (MulOpposite.unop m) โ†” IsUnit m
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem isAddUnit_unop {M : Type u_2} [AddMonoid M] {m : Mแตƒแต’แต–} :
          IsAddUnit (AddOpposite.unop m) โ†” IsAddUnit m