Documentation

Mathlib.Algebra.Group.Units.Defs

Units (i.e., invertible elements) of a monoid #

An element of a Monoid is a unit if it has a two-sided inverse.

Main declarations #

For both declarations, there is an additive counterpart: AddUnits and IsAddUnit. See also Prime, Associated, and Irreducible in Mathlib/Algebra/Associated.lean.

Notation #

We provide as notation for Units M, resembling the notation $R^{\times}$ for the units of a ring, which is common in mathematics.

TODO #

The results here should be used to golf the basic Group lemmas.

structure Units (α : Type u) [Monoid α] :

Units of a Monoid, bundled version. Notation: αˣ.

An element of a Monoid is a unit if it has a two-sided inverse. This version bundles the inverse element so that it can be computed. For a predicate see IsUnit.

  • val : α

    The underlying value in the base Monoid.

  • inv : α

    The inverse value of val in the base Monoid.

  • val_inv : self * self.inv = 1

    inv is the right inverse of val in the base Monoid.

  • inv_val : self.inv * self = 1

    inv is the left inverse of val in the base Monoid.

Instances For

    Units of a Monoid, bundled version. Notation: αˣ.

    An element of a Monoid is a unit if it has a two-sided inverse. This version bundles the inverse element so that it can be computed. For a predicate see IsUnit.

    Equations
      Instances For
        structure AddUnits (α : Type u) [AddMonoid α] :

        Units of an AddMonoid, bundled version.

        An element of an AddMonoid is a unit if it has a two-sided additive inverse. This version bundles the inverse element so that it can be computed. For a predicate see isAddUnit.

        Instances For
          instance Units.instCoeHead {α : Type u} [Monoid α] :
          CoeHead αˣ α

          A unit can be interpreted as a term in the base Monoid.

          Equations
            instance AddUnits.instCoeHead {α : Type u} [AddMonoid α] :

            An additive unit can be interpreted as a term in the base AddMonoid.

            Equations
              instance Units.instInv {α : Type u} [Monoid α] :

              The inverse of a unit in a Monoid.

              Equations
                instance AddUnits.instNeg {α : Type u} [AddMonoid α] :

                The additive inverse of an additive unit in an AddMonoid.

                Equations
                  def Units.Simps.val_inv {α : Type u} [Monoid α] (u : αˣ) :
                  α

                  See Note [custom simps projection]

                  Equations
                    Instances For
                      def AddUnits.Simps.val_neg {α : Type u} [AddMonoid α] (u : AddUnits α) :
                      α

                      See Note [custom simps projection]

                      Equations
                        Instances For
                          theorem Units.val_mk {α : Type u} [Monoid α] (a b : α) (h₁ : a * b = 1) (h₂ : b * a = 1) :
                          { val := a, inv := b, val_inv := h₁, inv_val := h₂ } = a
                          theorem AddUnits.val_mk {α : Type u} [AddMonoid α] (a b : α) (h₁ : a + b = 0) (h₂ : b + a = 0) :
                          { val := a, neg := b, val_neg := h₁, neg_val := h₂ } = a
                          theorem Units.ext_iff {α : Type u} [Monoid α] {a₁ a₂ : αˣ} :
                          a₁ = a₂ a₁ = a₂
                          theorem AddUnits.ext_iff {α : Type u} [AddMonoid α] {a₁ a₂ : AddUnits α} :
                          a₁ = a₂ a₁ = a₂
                          theorem Units.eq_iff {α : Type u} [Monoid α] {a b : αˣ} :
                          a = b a = b
                          theorem AddUnits.eq_iff {α : Type u} [AddMonoid α] {a b : AddUnits α} :
                          a = b a = b

                          Units have decidable equality if the base Monoid has decidable equality.

                          Equations

                            Additive units have decidable equality if the base AddMonoid has deciable equality.

                            Equations
                              @[simp]
                              theorem Units.mk_val {α : Type u} [Monoid α] (u : αˣ) (y : α) (h₁ : u * y = 1) (h₂ : y * u = 1) :
                              { val := u, inv := y, val_inv := h₁, inv_val := h₂ } = u
                              @[simp]
                              theorem AddUnits.mk_val {α : Type u} [AddMonoid α] (u : AddUnits α) (y : α) (h₁ : u + y = 0) (h₂ : y + u = 0) :
                              { val := u, neg := y, val_neg := h₁, neg_val := h₂ } = u
                              def Units.copy {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
                              αˣ

                              Copy a unit, adjusting definition equalities.

                              Equations
                                Instances For
                                  def AddUnits.copy {α : Type u} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :

                                  Copy an AddUnit, adjusting definitional equalities.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem AddUnits.val_neg_copy {α : Type u} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
                                      ↑(-u.copy val hv inv hi) = inv
                                      @[simp]
                                      theorem AddUnits.val_copy {α : Type u} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
                                      (u.copy val hv inv hi) = val
                                      @[simp]
                                      theorem Units.val_copy {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
                                      (u.copy val hv inv hi) = val
                                      @[simp]
                                      theorem Units.val_inv_copy {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
                                      (u.copy val hv inv hi)⁻¹ = inv
                                      theorem Units.copy_eq {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
                                      u.copy val hv inv hi = u
                                      theorem AddUnits.copy_eq {α : Type u} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
                                      u.copy val hv inv hi = u
                                      instance Units.instMul {α : Type u} [Monoid α] :

                                      Units of a monoid have an induced multiplication.

                                      Equations
                                        instance AddUnits.instAdd {α : Type u} [AddMonoid α] :

                                        Additive units of an additive monoid have an induced addition.

                                        Equations
                                          instance Units.instOne {α : Type u} [Monoid α] :

                                          Units of a monoid have a unit

                                          Equations
                                            instance AddUnits.instZero {α : Type u} [AddMonoid α] :

                                            Additive units of an additive monoid have a zero.

                                            Equations
                                              instance Units.instMulOneClass {α : Type u} [Monoid α] :

                                              Units of a monoid have a multiplication and multiplicative identity.

                                              Equations

                                                Additive units of an additive monoid have an addition and an additive identity.

                                                Equations
                                                  instance Units.instInhabited {α : Type u} [Monoid α] :

                                                  Units of a monoid are inhabited because 1 is a unit.

                                                  Equations

                                                    Additive units of an additive monoid are inhabited because 0 is an additive unit.

                                                    Equations
                                                      instance Units.instRepr {α : Type u} [Monoid α] [Repr α] :

                                                      Units of a monoid have a representation of the base value in the Monoid.

                                                      Equations
                                                        instance AddUnits.instRepr {α : Type u} [AddMonoid α] [Repr α] :

                                                        Additive units of an additive monoid have a representation of the base value in the AddMonoid.

                                                        Equations
                                                          @[simp]
                                                          theorem Units.val_mul {α : Type u} [Monoid α] (a b : αˣ) :
                                                          ↑(a * b) = a * b
                                                          @[simp]
                                                          theorem AddUnits.val_add {α : Type u} [AddMonoid α] (a b : AddUnits α) :
                                                          ↑(a + b) = a + b
                                                          @[simp]
                                                          theorem Units.val_one {α : Type u} [Monoid α] :
                                                          1 = 1
                                                          @[simp]
                                                          theorem AddUnits.val_zero {α : Type u} [AddMonoid α] :
                                                          0 = 0
                                                          @[simp]
                                                          theorem Units.val_eq_one {α : Type u} [Monoid α] {a : αˣ} :
                                                          a = 1 a = 1
                                                          @[simp]
                                                          theorem AddUnits.val_eq_zero {α : Type u} [AddMonoid α] {a : AddUnits α} :
                                                          a = 0 a = 0
                                                          @[simp]
                                                          theorem Units.inv_mk {α : Type u} [Monoid α] (x y : α) (h₁ : x * y = 1) (h₂ : y * x = 1) :
                                                          { val := x, inv := y, val_inv := h₁, inv_val := h₂ }⁻¹ = { val := y, inv := x, val_inv := h₂, inv_val := h₁ }
                                                          @[simp]
                                                          theorem AddUnits.neg_mk {α : Type u} [AddMonoid α] (x y : α) (h₁ : x + y = 0) (h₂ : y + x = 0) :
                                                          -{ val := x, neg := y, val_neg := h₁, neg_val := h₂ } = { val := y, neg := x, val_neg := h₂, neg_val := h₁ }
                                                          @[simp]
                                                          theorem Units.inv_eq_val_inv {α : Type u} [Monoid α] (a : αˣ) :
                                                          a.inv = a⁻¹
                                                          @[simp]
                                                          theorem AddUnits.neg_eq_val_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :
                                                          a.neg = ↑(-a)
                                                          @[simp]
                                                          theorem Units.inv_mul {α : Type u} [Monoid α] (a : αˣ) :
                                                          a⁻¹ * a = 1
                                                          @[simp]
                                                          theorem AddUnits.neg_add {α : Type u} [AddMonoid α] (a : AddUnits α) :
                                                          ↑(-a) + a = 0
                                                          @[simp]
                                                          theorem Units.mul_inv {α : Type u} [Monoid α] (a : αˣ) :
                                                          a * a⁻¹ = 1
                                                          @[simp]
                                                          theorem AddUnits.add_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :
                                                          a + ↑(-a) = 0
                                                          theorem Units.commute_coe_inv {α : Type u} [Monoid α] (a : αˣ) :
                                                          Commute a a⁻¹
                                                          theorem AddUnits.addCommute_coe_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :
                                                          AddCommute a ↑(-a)
                                                          theorem Units.commute_inv_coe {α : Type u} [Monoid α] (a : αˣ) :
                                                          Commute a⁻¹ a
                                                          theorem AddUnits.addCommute_neg_coe {α : Type u} [AddMonoid α] (a : AddUnits α) :
                                                          AddCommute ↑(-a) a
                                                          theorem Units.inv_mul_of_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : u = a) :
                                                          u⁻¹ * a = 1
                                                          theorem AddUnits.neg_add_of_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : u = a) :
                                                          ↑(-u) + a = 0
                                                          theorem Units.mul_inv_of_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : u = a) :
                                                          a * u⁻¹ = 1
                                                          theorem AddUnits.add_neg_of_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : u = a) :
                                                          a + ↑(-u) = 0
                                                          @[simp]
                                                          theorem Units.mul_inv_cancel_left {α : Type u} [Monoid α] (a : αˣ) (b : α) :
                                                          a * (a⁻¹ * b) = b
                                                          @[simp]
                                                          theorem AddUnits.add_neg_cancel_left {α : Type u} [AddMonoid α] (a : AddUnits α) (b : α) :
                                                          a + (↑(-a) + b) = b
                                                          @[simp]
                                                          theorem Units.inv_mul_cancel_left {α : Type u} [Monoid α] (a : αˣ) (b : α) :
                                                          a⁻¹ * (a * b) = b
                                                          @[simp]
                                                          theorem AddUnits.neg_add_cancel_left {α : Type u} [AddMonoid α] (a : AddUnits α) (b : α) :
                                                          ↑(-a) + (a + b) = b
                                                          theorem Units.inv_mul_eq_iff_eq_mul {α : Type u} [Monoid α] (a : αˣ) {b c : α} :
                                                          a⁻¹ * b = c b = a * c
                                                          theorem AddUnits.neg_add_eq_iff_eq_add {α : Type u} [AddMonoid α] (a : AddUnits α) {b c : α} :
                                                          ↑(-a) + b = c b = a + c
                                                          instance Units.instMonoid {α : Type u} [Monoid α] :
                                                          Equations
                                                            Equations
                                                              instance Units.instDiv {α : Type u} [Monoid α] :

                                                              Units of a monoid have division

                                                              Equations
                                                                instance AddUnits.instSub {α : Type u} [AddMonoid α] :

                                                                Additive units of an additive monoid have subtraction.

                                                                Equations

                                                                  Units of a monoid form a DivInvMonoid.

                                                                  Equations

                                                                    Additive units of an additive monoid form a SubNegMonoid.

                                                                    Equations
                                                                      instance Units.instGroup {α : Type u} [Monoid α] :

                                                                      Units of a monoid form a group.

                                                                      Equations

                                                                        Additive units of an additive monoid form an additive group.

                                                                        Equations

                                                                          Units of a commutative monoid form a commutative group.

                                                                          Equations

                                                                            Additive units of an additive commutative monoid form an additive commutative group.

                                                                            Equations
                                                                              @[simp]
                                                                              theorem Units.val_pow_eq_pow_val {α : Type u} [Monoid α] (a : αˣ) (n : ) :
                                                                              ↑(a ^ n) = a ^ n
                                                                              @[simp]
                                                                              theorem AddUnits.val_nsmul_eq_nsmul_val {α : Type u} [AddMonoid α] (a : AddUnits α) (n : ) :
                                                                              ↑(n a) = n a
                                                                              @[simp]
                                                                              theorem Units.val_inv_eq_inv_val {α : Type u} [DivisionMonoid α] (u : αˣ) :
                                                                              u⁻¹ = (↑u)⁻¹
                                                                              @[simp]
                                                                              theorem AddUnits.val_neg_eq_neg_val {α : Type u} [SubtractionMonoid α] (u : AddUnits α) :
                                                                              ↑(-u) = -u
                                                                              @[simp]
                                                                              theorem Units.val_div_eq_div_val {α : Type u} [DivisionMonoid α] (u₁ u₂ : αˣ) :
                                                                              ↑(u₁ / u₂) = u₁ / u₂
                                                                              @[simp]
                                                                              theorem AddUnits.val_sub_eq_sub_val {α : Type u} [SubtractionMonoid α] (u₁ u₂ : AddUnits α) :
                                                                              ↑(u₁ - u₂) = u₁ - u₂
                                                                              def Units.mkOfMulEqOne {α : Type u} [CommMonoid α] (a b : α) (hab : a * b = 1) :
                                                                              αˣ

                                                                              For a, b in a CommMonoid such that a * b = 1, makes a unit out of a.

                                                                              Equations
                                                                                Instances For
                                                                                  def AddUnits.mkOfAddEqZero {α : Type u} [AddCommMonoid α] (a b : α) (hab : a + b = 0) :

                                                                                  For a, b in an AddCommMonoid such that a + b = 0, makes an addUnit out of a.

                                                                                  Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem Units.val_mkOfMulEqOne {α : Type u} [CommMonoid α] {a b : α} (h : a * b = 1) :
                                                                                      (mkOfMulEqOne a b h) = a
                                                                                      @[simp]
                                                                                      theorem AddUnits.val_mkOfAddEqZero {α : Type u} [AddCommMonoid α] {a b : α} (h : a + b = 0) :
                                                                                      (mkOfAddEqZero a b h) = a
                                                                                      def divp {α : Type u} [Monoid α] (a : α) (u : αˣ) :
                                                                                      α

                                                                                      Partial division, denoted a /ₚ u. It is defined when the second argument is invertible, and unlike the division operator in DivisionRing it is not totalized at zero.

                                                                                      Equations
                                                                                        Instances For

                                                                                          Partial division, denoted a /ₚ u. It is defined when the second argument is invertible, and unlike the division operator in DivisionRing it is not totalized at zero.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem divp_self {α : Type u} [Monoid α] (u : αˣ) :
                                                                                              u /ₚ u = 1
                                                                                              @[simp]
                                                                                              theorem divp_one {α : Type u} [Monoid α] (a : α) :
                                                                                              a /ₚ 1 = a
                                                                                              theorem divp_assoc {α : Type u} [Monoid α] (a b : α) (u : αˣ) :
                                                                                              a * b /ₚ u = a * (b /ₚ u)
                                                                                              theorem divp_assoc' {α : Type u} [Monoid α] (x y : α) (u : αˣ) :
                                                                                              x * (y /ₚ u) = x * y /ₚ u

                                                                                              field_simp needs the reverse direction of divp_assoc to move all /ₚ to the right.

                                                                                              @[simp]
                                                                                              theorem divp_inv {α : Type u} [Monoid α] {a : α} (u : αˣ) :
                                                                                              a /ₚ u⁻¹ = a * u
                                                                                              @[simp]
                                                                                              theorem divp_mul_cancel {α : Type u} [Monoid α] (a : α) (u : αˣ) :
                                                                                              a /ₚ u * u = a
                                                                                              @[simp]
                                                                                              theorem mul_divp_cancel {α : Type u} [Monoid α] (a : α) (u : αˣ) :
                                                                                              a * u /ₚ u = a
                                                                                              theorem divp_divp_eq_divp_mul {α : Type u} [Monoid α] (x : α) (u₁ u₂ : αˣ) :
                                                                                              x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
                                                                                              @[simp]
                                                                                              theorem one_divp {α : Type u} [Monoid α] (u : αˣ) :
                                                                                              1 /ₚ u = u⁻¹
                                                                                              theorem inv_eq_one_divp {α : Type u} [Monoid α] (u : αˣ) :
                                                                                              u⁻¹ = 1 /ₚ u

                                                                                              Used for field_simp to deal with inverses of units.

                                                                                              theorem val_div_eq_divp {α : Type u} [Monoid α] (u₁ u₂ : αˣ) :
                                                                                              ↑(u₁ / u₂) = u₁ /ₚ u₂

                                                                                              field_simp moves division inside αˣ to the right, and this lemma lifts the calculation to α.

                                                                                              IsUnit predicate #

                                                                                              def IsUnit {M : Type u_1} [Monoid M] (a : M) :

                                                                                              An element a : M of a Monoid is a unit if it has a two-sided inverse. The actual definition says that a is equal to some u : Mˣ, where is a bundled version of IsUnit.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  def IsAddUnit {M : Type u_1} [AddMonoid M] (a : M) :

                                                                                                  An element a : M of an AddMonoid is an AddUnit if it has a two-sided additive inverse. The actual definition says that a is equal to some u : AddUnits M, where AddUnits M is a bundled version of IsAddUnit.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      theorem isUnit_iff_exists {M : Type u_1} [Monoid M] {x : M} :
                                                                                                      IsUnit x (b : M), x * b = 1 b * x = 1

                                                                                                      See isUnit_iff_exists_and_exists for a similar lemma with two existentials.

                                                                                                      theorem isAddUnit_iff_exists {M : Type u_1} [AddMonoid M] {x : M} :
                                                                                                      IsAddUnit x (b : M), x + b = 0 b + x = 0

                                                                                                      See isAddUnit_iff_exists_and_exists for a similar lemma with two existentials.

                                                                                                      theorem isUnit_iff_exists_and_exists {M : Type u_1} [Monoid M] {a : M} :
                                                                                                      IsUnit a ( (b : M), a * b = 1) (c : M), c * a = 1

                                                                                                      See isUnit_iff_exists for a similar lemma with one existential.

                                                                                                      theorem isAddUnit_iff_exists_and_exists {M : Type u_1} [AddMonoid M] {a : M} :
                                                                                                      IsAddUnit a ( (b : M), a + b = 0) (c : M), c + a = 0

                                                                                                      See isAddUnit_iff_exists for a similar lemma with one existential.

                                                                                                      @[simp]
                                                                                                      theorem Units.isUnit {M : Type u_1} [Monoid M] (u : Mˣ) :
                                                                                                      IsUnit u
                                                                                                      @[simp]
                                                                                                      theorem AddUnits.isAddUnit {M : Type u_1} [AddMonoid M] (u : AddUnits M) :
                                                                                                      @[simp]
                                                                                                      theorem isUnit_one {M : Type u_1} [Monoid M] :
                                                                                                      @[simp]
                                                                                                      theorem isAddUnit_zero {M : Type u_1} [AddMonoid M] :
                                                                                                      theorem isUnit_of_mul_eq_one {M : Type u_1} [CommMonoid M] (a b : M) (h : a * b = 1) :
                                                                                                      theorem isAddUnit_of_add_eq_zero {M : Type u_1} [AddCommMonoid M] (a b : M) (h : a + b = 0) :
                                                                                                      theorem isUnit_of_mul_eq_one_right {M : Type u_1} [CommMonoid M] (a b : M) (h : a * b = 1) :
                                                                                                      theorem isAddUnit_of_add_eq_zero_right {M : Type u_1} [AddCommMonoid M] (a b : M) (h : a + b = 0) :
                                                                                                      theorem IsUnit.exists_right_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
                                                                                                      (b : M), a * b = 1
                                                                                                      theorem IsAddUnit.exists_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
                                                                                                      (b : M), a + b = 0
                                                                                                      theorem IsUnit.exists_left_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
                                                                                                      (b : M), b * a = 1
                                                                                                      theorem IsAddUnit.exists_neg' {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
                                                                                                      (b : M), b + a = 0
                                                                                                      theorem IsUnit.mul {M : Type u_1} [Monoid M] {a b : M} :
                                                                                                      IsUnit aIsUnit bIsUnit (a * b)
                                                                                                      theorem IsAddUnit.add {M : Type u_1} [AddMonoid M] {a b : M} :
                                                                                                      IsAddUnit aIsAddUnit bIsAddUnit (a + b)
                                                                                                      theorem IsUnit.pow {M : Type u_1} [Monoid M] {a : M} (n : ) :
                                                                                                      IsUnit aIsUnit (a ^ n)
                                                                                                      theorem IsAddUnit.nsmul {M : Type u_1} [AddMonoid M] {a : M} (n : ) :
                                                                                                      IsAddUnit aIsAddUnit (n a)
                                                                                                      @[simp]
                                                                                                      theorem isUnit_iff_eq_one {M : Type u_1} [Monoid M] [Subsingleton Mˣ] {x : M} :
                                                                                                      IsUnit x x = 1
                                                                                                      @[simp]
                                                                                                      theorem isAddUnit_iff_eq_zero {M : Type u_1} [AddMonoid M] [Subsingleton (AddUnits M)] {x : M} :
                                                                                                      theorem isUnit_iff_exists_inv {M : Type u_1} [CommMonoid M] {a : M} :
                                                                                                      IsUnit a (b : M), a * b = 1
                                                                                                      theorem isAddUnit_iff_exists_neg {M : Type u_1} [AddCommMonoid M] {a : M} :
                                                                                                      IsAddUnit a (b : M), a + b = 0
                                                                                                      theorem isUnit_iff_exists_inv' {M : Type u_1} [CommMonoid M] {a : M} :
                                                                                                      IsUnit a (b : M), b * a = 1
                                                                                                      theorem isAddUnit_iff_exists_neg' {M : Type u_1} [AddCommMonoid M] {a : M} :
                                                                                                      IsAddUnit a (b : M), b + a = 0
                                                                                                      @[simp]
                                                                                                      theorem Units.isUnit_mul_units {M : Type u_1} [Monoid M] (a : M) (u : Mˣ) :
                                                                                                      IsUnit (a * u) IsUnit a

                                                                                                      Multiplication by a u : Mˣ on the right doesn't affect IsUnit.

                                                                                                      @[simp]
                                                                                                      theorem AddUnits.isAddUnit_add_addUnits {M : Type u_1} [AddMonoid M] (a : M) (u : AddUnits M) :

                                                                                                      Addition of a u : AddUnits M on the right doesn't affect IsAddUnit.

                                                                                                      @[simp]
                                                                                                      theorem Units.isUnit_units_mul {M : Type u_3} [Monoid M] (u : Mˣ) (a : M) :
                                                                                                      IsUnit (u * a) IsUnit a

                                                                                                      Multiplication by a u : Mˣ on the left doesn't affect IsUnit.

                                                                                                      @[simp]
                                                                                                      theorem AddUnits.isAddUnit_addUnits_add {M : Type u_3} [AddMonoid M] (u : AddUnits M) (a : M) :

                                                                                                      Addition of a u : AddUnits M on the left doesn't affect IsAddUnit.

                                                                                                      theorem isUnit_of_mul_isUnit_left {M : Type u_1} [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) :
                                                                                                      theorem isAddUnit_of_add_isAddUnit_left {M : Type u_1} [AddCommMonoid M] {x y : M} (hu : IsAddUnit (x + y)) :
                                                                                                      theorem isUnit_of_mul_isUnit_right {M : Type u_1} [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) :
                                                                                                      theorem isAddUnit_of_add_isAddUnit_right {M : Type u_1} [AddCommMonoid M] {x y : M} (hu : IsAddUnit (x + y)) :
                                                                                                      @[simp]
                                                                                                      theorem IsUnit.mul_iff {M : Type u_1} [CommMonoid M] {x y : M} :
                                                                                                      @[simp]
                                                                                                      theorem IsAddUnit.add_iff {M : Type u_1} [AddCommMonoid M] {x y : M} :
                                                                                                      noncomputable def IsUnit.unit {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :

                                                                                                      The element of the group of units, corresponding to an element of a monoid which is a unit. When α is a DivisionMonoid, use IsUnit.unit' instead.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          noncomputable def IsAddUnit.addUnit {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :

                                                                                                          The element of the additive group of additive units, corresponding to an element of an additive monoid which is an additive unit. When α is a SubtractionMonoid, use IsAddUnit.addUnit' instead.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem IsUnit.unit_of_val_units {M : Type u_1} [Monoid M] {a : Mˣ} (h : IsUnit a) :
                                                                                                              h.unit = a
                                                                                                              @[simp]
                                                                                                              theorem IsAddUnit.addUnit_of_val_addUnits {M : Type u_1} [AddMonoid M] {a : AddUnits M} (h : IsAddUnit a) :
                                                                                                              @[simp]
                                                                                                              theorem IsUnit.unit_spec {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
                                                                                                              h.unit = a
                                                                                                              @[simp]
                                                                                                              theorem IsAddUnit.addUnit_spec {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
                                                                                                              h.addUnit = a
                                                                                                              @[simp]
                                                                                                              theorem IsUnit.unit_one {M : Type u_1} [Monoid M] (h : IsUnit 1) :
                                                                                                              h.unit = 1
                                                                                                              @[simp]
                                                                                                              theorem IsAddUnit.addUnit_zero {M : Type u_1} [AddMonoid M] (h : IsAddUnit 0) :
                                                                                                              @[simp]
                                                                                                              theorem IsUnit.val_inv_mul {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
                                                                                                              h.unit⁻¹ * a = 1
                                                                                                              @[simp]
                                                                                                              theorem IsAddUnit.val_neg_add {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
                                                                                                              ↑(-h.addUnit) + a = 0
                                                                                                              @[simp]
                                                                                                              theorem IsUnit.mul_val_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
                                                                                                              a * h.unit⁻¹ = 1
                                                                                                              @[simp]
                                                                                                              theorem IsAddUnit.add_val_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
                                                                                                              a + ↑(-h.addUnit) = 0
                                                                                                              instance IsUnit.instDecidableOfExistsUnitsEqVal {M : Type u_1} [Monoid M] (x : M) [h : Decidable ( (u : Mˣ), u = x)] :

                                                                                                              IsUnit x is decidable if we can decide if x comes from .

                                                                                                              Equations

                                                                                                                IsAddUnit x is decidable if we can decide if x comes from AddUnits M.

                                                                                                                Equations
                                                                                                                  @[simp]
                                                                                                                  theorem IsUnit.inv_mul_cancel {α : Type u} [DivisionMonoid α] {a : α} :
                                                                                                                  IsUnit aa⁻¹ * a = 1
                                                                                                                  @[simp]
                                                                                                                  theorem IsAddUnit.neg_add_cancel {α : Type u} [SubtractionMonoid α] {a : α} :
                                                                                                                  IsAddUnit a-a + a = 0
                                                                                                                  @[simp]
                                                                                                                  theorem IsUnit.mul_inv_cancel {α : Type u} [DivisionMonoid α] {a : α} :
                                                                                                                  IsUnit aa * a⁻¹ = 1
                                                                                                                  @[simp]
                                                                                                                  theorem IsAddUnit.add_neg_cancel {α : Type u} [SubtractionMonoid α] {a : α} :
                                                                                                                  IsAddUnit aa + -a = 0
                                                                                                                  def IsUnit.unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
                                                                                                                  αˣ

                                                                                                                  The element of the group of units, corresponding to an element of a monoid which is a unit. As opposed to IsUnit.unit, the inverse is computable and comes from the inversion on α. This is useful to transfer properties of inversion in Units α to α. See also toUnits.

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      def IsAddUnit.addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :

                                                                                                                      The element of the additive group of additive units, corresponding to an element of an additive monoid which is an additive unit. As opposed to IsAddUnit.addUnit, the negation is computable and comes from the negation on α. This is useful to transfer properties of negation in AddUnits α to α. See also toAddUnits.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem IsAddUnit.val_addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
                                                                                                                          h.addUnit' = a
                                                                                                                          @[simp]
                                                                                                                          theorem IsUnit.val_unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
                                                                                                                          h.unit' = a
                                                                                                                          theorem IsUnit.val_inv_unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
                                                                                                                          theorem IsAddUnit.val_neg_addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
                                                                                                                          ↑(-h.addUnit') = -a
                                                                                                                          @[simp]
                                                                                                                          theorem IsUnit.mul_inv_cancel_left {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :
                                                                                                                          a * (a⁻¹ * b) = b
                                                                                                                          @[simp]
                                                                                                                          theorem IsAddUnit.add_neg_cancel_left {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
                                                                                                                          a + (-a + b) = b
                                                                                                                          @[simp]
                                                                                                                          theorem IsUnit.inv_mul_cancel_left {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :
                                                                                                                          a⁻¹ * (a * b) = b
                                                                                                                          @[simp]
                                                                                                                          theorem IsAddUnit.neg_add_cancel_left {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
                                                                                                                          -a + (a + b) = b
                                                                                                                          theorem IsUnit.div_self {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
                                                                                                                          a / a = 1
                                                                                                                          theorem IsAddUnit.sub_self {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
                                                                                                                          a - a = 0
                                                                                                                          theorem IsUnit.inv {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
                                                                                                                          theorem IsAddUnit.neg {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
                                                                                                                          theorem IsUnit.div {α : Type u} [DivisionMonoid α] {a b : α} (ha : IsUnit a) (hb : IsUnit b) :
                                                                                                                          IsUnit (a / b)
                                                                                                                          theorem IsAddUnit.sub {α : Type u} [SubtractionMonoid α] {a b : α} (ha : IsAddUnit a) (hb : IsAddUnit b) :
                                                                                                                          IsAddUnit (a - b)
                                                                                                                          theorem IsUnit.div_mul_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
                                                                                                                          b / (a * b) = a⁻¹
                                                                                                                          theorem IsAddUnit.sub_add_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
                                                                                                                          b - (a + b) = -a
                                                                                                                          theorem IsUnit.mul_div_mul_right {α : Type u} [DivisionMonoid α] {c : α} (h : IsUnit c) (a b : α) :
                                                                                                                          a * c / (b * c) = a / b
                                                                                                                          theorem IsAddUnit.add_sub_add_right {α : Type u} [SubtractionMonoid α] {c : α} (h : IsAddUnit c) (a b : α) :
                                                                                                                          a + c - (b + c) = a - b
                                                                                                                          theorem IsUnit.div_mul_cancel_left {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
                                                                                                                          a / (a * b) = b⁻¹
                                                                                                                          theorem IsAddUnit.sub_add_cancel_left {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
                                                                                                                          a - (a + b) = -b
                                                                                                                          theorem IsUnit.mul_div_mul_left {α : Type u} [DivisionCommMonoid α] {c : α} (h : IsUnit c) (a b : α) :
                                                                                                                          c * a / (c * b) = a / b
                                                                                                                          theorem IsAddUnit.add_sub_add_left {α : Type u} [SubtractionCommMonoid α] {c : α} (h : IsAddUnit c) (a b : α) :
                                                                                                                          c + a - (c + b) = a - b
                                                                                                                          theorem divp_eq_div {α : Type u} [DivisionMonoid α] (a : α) (u : αˣ) :
                                                                                                                          a /ₚ u = a / u
                                                                                                                          theorem Group.isUnit {α : Type u} [Group α] (a : α) :
                                                                                                                          theorem AddGroup.isAddUnit {α : Type u} [AddGroup α] (a : α) :
                                                                                                                          noncomputable def invOfIsUnit {M : Type u_1} [Monoid M] (h : ∀ (a : M), IsUnit a) :
                                                                                                                          Inv M

                                                                                                                          Constructs an inv operation for a Monoid consisting only of units.

                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              noncomputable def groupOfIsUnit {M : Type u_1} [hM : Monoid M] (h : ∀ (a : M), IsUnit a) :

                                                                                                                              Constructs a Group structure on a Monoid consisting only of units.

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  noncomputable def commGroupOfIsUnit {M : Type u_1} [hM : CommMonoid M] (h : ∀ (a : M), IsUnit a) :

                                                                                                                                  Constructs a CommGroup structure on a CommMonoid consisting only of units.

                                                                                                                                  Equations
                                                                                                                                    Instances For