Documentation

Mathlib.Algebra.Group.Units.Opposite

Units in multiplicative and additive opposites #

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

Equations
    Instances For

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

      Equations
        Instances For
          theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) :
          theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) :
          theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) :
          @[simp]
          theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} :
          @[simp]
          theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} :
          @[simp]
          theorem isUnit_unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} :