Documentation

Mathlib.Algebra.Group.Units

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.

Notation #

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

structure Units (α : Type u) [inst : Monoid α] :
  • The underlying value in the base Monoid.

    val : α
  • The inverse value of val in the base Monoid.

    inv : α
  • inv is the right inverse of val in the base Monoid.

    val_inv : val * inv = 1
  • inv is the left inverse of val in the base Monoid.

    inv_val : inv * val = 1

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.

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
    structure AddUnits (α : Type u) [inst : AddMonoid α] :
    • The underlying value in the base AddMonoid.

      val : α
    • The additive inverse value of val in the base AddMonoid.

      neg : α
    • neg is the right additive inverse of val in the base AddMonoid.

      val_neg : val + neg = 0
    • neg is the left additive inverse of val in the base AddMonoid.

      neg_val : neg + val = 0

    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
      theorem unique_zero {α : Type u_1} [inst : Unique α] [inst : Zero α] :
      default = 0
      theorem unique_one {α : Type u_1} [inst : Unique α] [inst : One α] :
      default = 1
      instance AddUnits.instCoeHeadAddUnits {α : Type u} [inst : AddMonoid α] :

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

      Equations
      • AddUnits.instCoeHeadAddUnits = { coe := AddUnits.val }
      instance Units.instCoeHeadUnits {α : Type u} [inst : Monoid α] :
      CoeHead αˣ α

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

      Equations
      • Units.instCoeHeadUnits = { coe := Units.val }
      instance AddUnits.instNegAddUnits {α : Type u} [inst : AddMonoid α] :

      The additive inverse of an additive unit in an AddMonoid.

      Equations
      • AddUnits.instNegAddUnits = { neg := fun u => { val := u.neg, neg := u, val_neg := (_ : u.neg + u = 0), neg_val := (_ : u + u.neg = 0) } }
      instance Units.instInvUnits {α : Type u} [inst : Monoid α] :

      The inverse of a unit in a Monoid.

      Equations
      • Units.instInvUnits = { inv := fun u => { val := u.inv, inv := u, val_inv := (_ : u.inv * u = 1), inv_val := (_ : u * u.inv = 1) } }
      theorem AddUnits.val_mk {α : Type u} [inst : AddMonoid α] (a : α) (b : α) (h₁ : a + b = 0) (h₂ : b + a = 0) :
      { val := a, neg := b, val_neg := h₁, neg_val := h₂ } = a
      theorem Units.val_mk {α : Type u} [inst : Monoid α] (a : α) (b : α) (h₁ : a * b = 1) (h₂ : b * a = 1) :
      { val := a, inv := b, val_inv := h₁, inv_val := h₂ } = a
      theorem AddUnits.ext {α : Type u} [inst : AddMonoid α] :
      Function.Injective fun u => u
      abbrev AddUnits.ext.match_1 {α : Type u_1} [inst : AddMonoid α] (motive : (x x_1 : AddUnits α) → (fun u => u) x = (fun u => u) x_1Prop) :
      (x x_1 : AddUnits α) → (x_2 : (fun u => u) x = (fun u => u) x_1) → ((v i₁ : α) → (vi₁ : v + i₁ = 0) → (iv₁ : i₁ + v = 0) → (v' i₂ : α) → (vi₂ : v' + i₂ = 0) → (iv₂ : i₂ + v' = 0) → (e : (fun u => u) { val := v, neg := i₁, val_neg := vi₁, neg_val := iv₁ } = (fun u => u) { val := v', neg := i₂, val_neg := vi₂, neg_val := iv₂ }) → motive { val := v, neg := i₁, val_neg := vi₁, neg_val := iv₁ } { val := v', neg := i₂, val_neg := vi₂, neg_val := iv₂ } e) → motive x x_1 x_2
      Equations
      • One or more equations did not get rendered due to their size.
      theorem Units.ext {α : Type u} [inst : Monoid α] :
      Function.Injective fun u => u
      theorem AddUnits.eq_iff {α : Type u} [inst : AddMonoid α] {a : AddUnits α} {b : AddUnits α} :
      a = b a = b
      theorem Units.eq_iff {α : Type u} [inst : Monoid α] {a : αˣ} {b : αˣ} :
      a = b a = b
      theorem AddUnits.ext_iff {α : Type u} [inst : AddMonoid α] {a : AddUnits α} {b : AddUnits α} :
      a = b a = b
      theorem Units.ext_iff {α : Type u} [inst : Monoid α] {a : αˣ} {b : αˣ} :
      a = b a = b
      instance AddUnits.instDecidableEqAddUnits {α : Type u} [inst : AddMonoid α] [inst : DecidableEq α] :

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

      Equations
      instance Units.instDecidableEqUnits {α : Type u} [inst : Monoid α] [inst : DecidableEq α] :

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

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

      Copy an AddUnit, adjusting definitional equalities.

      Equations
      • AddUnits.copy u val hv inv hi = { val := val, neg := inv, val_neg := (_ : val + inv = 0), neg_val := (_ : inv + val = 0) }
      def AddUnits.copy.proof_2 {α : Type u_1} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
      inv + val = 0
      Equations
      • (_ : inv + val = 0) = (_ : inv + val = 0)
      def AddUnits.copy.proof_1 {α : Type u_1} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
      val + inv = 0
      Equations
      • (_ : val + inv = 0) = (_ : val + inv = 0)
      @[simp]
      theorem AddUnits.copy_val {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
      ↑(AddUnits.copy u val hv inv hi) = val
      @[simp]
      theorem Units.copy_val {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
      ↑(Units.copy u val hv inv hi) = val
      @[simp]
      theorem AddUnits.copy_neg {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
      (AddUnits.copy u val hv inv hi).neg = inv
      @[simp]
      theorem Units.copy_inv {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
      (Units.copy u val hv inv hi).inv = inv
      def Units.copy {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
      αˣ

      Copy a unit, adjusting definition equalities.

      Equations
      • Units.copy u val hv inv hi = { val := val, inv := inv, val_inv := (_ : val * inv = 1), inv_val := (_ : inv * val = 1) }
      theorem AddUnits.copy_eq {α : Type u} [inst : AddMonoid α] (u : AddUnits α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(-u)) :
      AddUnits.copy u val hv inv hi = u
      theorem Units.copy_eq {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = u) (inv : α) (hi : inv = u⁻¹) :
      Units.copy u val hv inv hi = u

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

      Equations
      def AddUnits.instAddZeroClassAddUnits.proof_4 {α : Type u_1} [inst : AddMonoid α] (u : AddUnits α) :
      0 + u = u
      Equations
      • (_ : 0 + u = u) = (_ : 0 + u = u)
      def AddUnits.instAddZeroClassAddUnits.proof_2 {α : Type u_1} [inst : AddMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :
      u₁ + u₂ + (u₂.neg + u₁.neg) = 0
      Equations
      • (_ : u₁ + u₂ + (u₂.neg + u₁.neg) = 0) = (_ : u₁ + u₂ + (u₂.neg + u₁.neg) = 0)
      def AddUnits.instAddZeroClassAddUnits.proof_3 {α : Type u_1} [inst : AddMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :
      u₂.neg + u₁.neg + (u₁ + u₂) = 0
      Equations
      • (_ : u₂.neg + u₁.neg + (u₁ + u₂) = 0) = (_ : u₂.neg + u₁.neg + (u₁ + u₂) = 0)
      def AddUnits.instAddZeroClassAddUnits.proof_5 {α : Type u_1} [inst : AddMonoid α] (u : AddUnits α) :
      u + 0 = u
      Equations
      • (_ : u + 0 = u) = (_ : u + 0 = u)
      def AddUnits.instAddZeroClassAddUnits.proof_1 {α : Type u_1} [inst : AddMonoid α] :
      0 + 0 = 0
      Equations
      • (_ : 0 + 0 = 0) = (_ : 0 + 0 = 0)
      instance Units.instMulOneClassUnits {α : Type u} [inst : Monoid α] :

      Units of a monoid form have a multiplication and multiplicative identity.

      Equations
      def AddUnits.instAddGroupAddUnits.proof_11 {α : Type u_1} [inst : AddMonoid α] (u : AddUnits α) :
      -u + u = 0
      Equations
      • (_ : -u + u = 0) = (_ : -u + u = 0)
      def AddUnits.instAddGroupAddUnits.proof_2 {α : Type u_1} [inst : AddMonoid α] (a : AddUnits α) :
      0 + a = a
      Equations
      def AddUnits.instAddGroupAddUnits.proof_6 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (x x_1 x_2 : AddUnits α), x + x_1 + x_2 = x + (x_1 + x_2)
      Equations
      • (_ : x + x + x = x + (x + x)) = (_ : x + x + x = x + (x + x))
      def AddUnits.instAddGroupAddUnits.proof_7 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (a b : AddUnits α), a - b = a - b
      Equations
      • (_ : a - b = a - b) = (_ : a - b = a - b)
      def AddUnits.instAddGroupAddUnits.proof_8 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (a : AddUnits α), zsmulRec 0 a = zsmulRec 0 a
      Equations
      • (_ : zsmulRec 0 a = zsmulRec 0 a) = (_ : zsmulRec 0 a = zsmulRec 0 a)
      def AddUnits.instAddGroupAddUnits.proof_10 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (n : ) (a : AddUnits α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a
      Equations
      def AddUnits.instAddGroupAddUnits.proof_3 {α : Type u_1} [inst : AddMonoid α] (a : AddUnits α) :
      a + 0 = a
      Equations
      def AddUnits.instAddGroupAddUnits.proof_5 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (n : ) (x : AddUnits α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
      Equations
      • (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)
      def AddUnits.instAddGroupAddUnits.proof_1 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (x x_1 x_2 : AddUnits α), x + x_1 + x_2 = x + (x_1 + x_2)
      Equations
      • (_ : x + x + x = x + (x + x)) = (_ : x + x + x = x + (x + x))
      instance AddUnits.instAddGroupAddUnits {α : Type u} [inst : AddMonoid α] :

      Additive units of an additive monoid form an additive group.

      Equations
      def AddUnits.instAddGroupAddUnits.proof_9 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (n : ) (a : AddUnits α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a
      Equations
      def AddUnits.instAddGroupAddUnits.proof_4 {α : Type u_1} [inst : AddMonoid α] :
      ∀ (x : AddUnits α), nsmulRec 0 x = nsmulRec 0 x
      Equations
      • (_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)
      instance Units.instGroupUnits {α : Type u} [inst : Monoid α] :

      Units of a monoid form a group.

      Equations
      • Units.instGroupUnits = let src := inferInstance; Group.mk (_ : ∀ (u : αˣ), u⁻¹ * u = 1)
      Equations
      def AddUnits.instAddCommGroupAddUnitsToAddMonoid.proof_2 {α : Type u_1} [inst : AddCommMonoid α] :
      ∀ (x x_1 : AddUnits α), x + x_1 = x_1 + x
      Equations
      • (_ : x + x = x + x) = (_ : x + x = x + x)

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

      Equations
      • AddUnits.instAddCommGroupAddUnitsToAddMonoid = let src := inferInstance; AddCommGroup.mk (_ : ∀ (x x_1 : AddUnits α), x + x_1 = x_1 + x)
      instance Units.instCommGroupUnitsToMonoid {α : Type u_1} [inst : CommMonoid α] :

      Units of a commutative monoid form a commutative group.

      Equations
      • Units.instCommGroupUnitsToMonoid = let src := inferInstance; CommGroup.mk (_ : ∀ (x x_1 : αˣ), x * x_1 = x_1 * x)
      instance AddUnits.instInhabitedAddUnits {α : Type u} [inst : AddMonoid α] :

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

      Equations
      • AddUnits.instInhabitedAddUnits = { default := 0 }
      instance Units.instInhabitedUnits {α : Type u} [inst : Monoid α] :

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

      Equations
      • Units.instInhabitedUnits = { default := 1 }
      instance AddUnits.instReprAddUnits {α : Type u} [inst : AddMonoid α] [inst : Repr α] :

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

      Equations
      • AddUnits.instReprAddUnits = { reprPrec := reprPrec AddUnits.val }
      instance Units.instReprUnits {α : Type u} [inst : Monoid α] [inst : Repr α] :

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

      Equations
      • Units.instReprUnits = { reprPrec := reprPrec Units.val }
      @[simp]
      theorem AddUnits.val_add {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : AddUnits α) :
      ↑(a + b) = a + b
      @[simp]
      theorem Units.val_mul {α : Type u} [inst : Monoid α] (a : αˣ) (b : αˣ) :
      ↑(a * b) = a * b
      @[simp]
      theorem AddUnits.val_zero {α : Type u} [inst : AddMonoid α] :
      0 = 0
      @[simp]
      theorem Units.val_one {α : Type u} [inst : Monoid α] :
      1 = 1
      @[simp]
      theorem AddUnits.val_eq_zero {α : Type u} [inst : AddMonoid α] {a : AddUnits α} :
      a = 0 a = 0
      @[simp]
      theorem Units.val_eq_one {α : Type u} [inst : Monoid α] {a : αˣ} :
      a = 1 a = 1
      @[simp]
      theorem AddUnits.neg_mk {α : Type u} [inst : 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_mk {α : Type u} [inst : 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_eq_val_neg {α : Type u} [inst : AddMonoid α] (a : AddUnits α) :
      a.neg = ↑(-a)
      @[simp]
      theorem Units.inv_eq_val_inv {α : Type u} [inst : Monoid α] (a : αˣ) :
      a.inv = a⁻¹
      @[simp]
      theorem AddUnits.neg_add {α : Type u} [inst : AddMonoid α] (a : AddUnits α) :
      ↑(-a) + a = 0
      @[simp]
      theorem Units.inv_mul {α : Type u} [inst : Monoid α] (a : αˣ) :
      a⁻¹ * a = 1
      @[simp]
      theorem AddUnits.add_neg {α : Type u} [inst : AddMonoid α] (a : AddUnits α) :
      a + ↑(-a) = 0
      @[simp]
      theorem Units.mul_inv {α : Type u} [inst : Monoid α] (a : αˣ) :
      a * a⁻¹ = 1
      theorem AddUnits.neg_add_of_eq {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} (h : u = a) :
      ↑(-u) + a = 0
      theorem Units.inv_mul_of_eq {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} (h : u = a) :
      u⁻¹ * a = 1
      theorem AddUnits.add_neg_of_eq {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} (h : u = a) :
      a + ↑(-u) = 0
      theorem Units.mul_inv_of_eq {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} (h : u = a) :
      a * u⁻¹ = 1
      @[simp]
      theorem AddUnits.add_neg_cancel_left {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : α) :
      a + (↑(-a) + b) = b
      @[simp]
      theorem Units.mul_inv_cancel_left {α : Type u} [inst : Monoid α] (a : αˣ) (b : α) :
      a * (a⁻¹ * b) = b
      @[simp]
      theorem AddUnits.neg_add_cancel_left {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : α) :
      ↑(-a) + (a + b) = b
      @[simp]
      theorem Units.inv_mul_cancel_left {α : Type u} [inst : Monoid α] (a : αˣ) (b : α) :
      a⁻¹ * (a * b) = b
      @[simp]
      theorem AddUnits.add_neg_cancel_right {α : Type u} [inst : AddMonoid α] (a : α) (b : AddUnits α) :
      a + b + ↑(-b) = a
      @[simp]
      theorem Units.mul_inv_cancel_right {α : Type u} [inst : Monoid α] (a : α) (b : αˣ) :
      a * b * b⁻¹ = a
      @[simp]
      theorem AddUnits.neg_add_cancel_right {α : Type u} [inst : AddMonoid α] (a : α) (b : AddUnits α) :
      a + ↑(-b) + b = a
      @[simp]
      theorem Units.inv_mul_cancel_right {α : Type u} [inst : Monoid α] (a : α) (b : αˣ) :
      a * b⁻¹ * b = a
      @[simp]
      theorem AddUnits.add_right_inj {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b : α} {c : α} :
      a + b = a + c b = c
      @[simp]
      theorem Units.mul_right_inj {α : Type u} [inst : Monoid α] (a : αˣ) {b : α} {c : α} :
      a * b = a * c b = c
      @[simp]
      theorem AddUnits.add_left_inj {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b : α} {c : α} :
      b + a = c + a b = c
      @[simp]
      theorem Units.mul_left_inj {α : Type u} [inst : Monoid α] (a : αˣ) {b : α} {c : α} :
      b * a = c * a b = c
      theorem AddUnits.eq_add_neg_iff_add_eq {α : Type u} [inst : AddMonoid α] (c : AddUnits α) {a : α} {b : α} :
      a = b + ↑(-c) a + c = b
      theorem Units.eq_mul_inv_iff_mul_eq {α : Type u} [inst : Monoid α] (c : αˣ) {a : α} {b : α} :
      a = b * c⁻¹ a * c = b
      theorem AddUnits.eq_neg_add_iff_add_eq {α : Type u} [inst : AddMonoid α] (b : AddUnits α) {a : α} {c : α} :
      a = ↑(-b) + c b + a = c
      theorem Units.eq_inv_mul_iff_mul_eq {α : Type u} [inst : Monoid α] (b : αˣ) {a : α} {c : α} :
      a = b⁻¹ * c b * a = c
      theorem AddUnits.neg_add_eq_iff_eq_add {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b : α} {c : α} :
      ↑(-a) + b = c b = a + c
      theorem Units.inv_mul_eq_iff_eq_mul {α : Type u} [inst : Monoid α] (a : αˣ) {b : α} {c : α} :
      a⁻¹ * b = c b = a * c
      theorem AddUnits.add_neg_eq_iff_eq_add {α : Type u} [inst : AddMonoid α] (b : AddUnits α) {a : α} {c : α} :
      a + ↑(-b) = c a = c + b
      theorem Units.mul_inv_eq_iff_eq_mul {α : Type u} [inst : Monoid α] (b : αˣ) {a : α} {c : α} :
      a * b⁻¹ = c a = c * b
      theorem AddUnits.neg_eq_of_add_eq_zero_left {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} (h : a + u = 0) :
      ↑(-u) = a
      theorem Units.inv_eq_of_mul_eq_one_left {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} (h : a * u = 1) :
      u⁻¹ = a
      theorem AddUnits.neg_eq_of_add_eq_zero_right {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} (h : u + a = 0) :
      ↑(-u) = a
      theorem Units.inv_eq_of_mul_eq_one_right {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} (h : u * a = 1) :
      u⁻¹ = a
      theorem AddUnits.eq_neg_of_add_eq_zero_left {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} (h : u + a = 0) :
      a = ↑(-u)
      theorem Units.eq_inv_of_mul_eq_one_left {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} (h : u * a = 1) :
      a = u⁻¹
      theorem AddUnits.eq_neg_of_add_eq_zero_right {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} (h : a + u = 0) :
      a = ↑(-u)
      theorem Units.eq_inv_of_mul_eq_one_right {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} (h : a * u = 1) :
      a = u⁻¹
      @[simp]
      theorem AddUnits.add_neg_eq_zero {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} :
      a + ↑(-u) = 0 a = u
      @[simp]
      theorem Units.mul_inv_eq_one {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} :
      a * u⁻¹ = 1 a = u
      @[simp]
      theorem AddUnits.neg_add_eq_zero {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} :
      ↑(-u) + a = 0 u = a
      @[simp]
      theorem Units.inv_mul_eq_one {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} :
      u⁻¹ * a = 1 u = a
      theorem AddUnits.add_eq_zero_iff_eq_neg {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} :
      a + u = 0 a = ↑(-u)
      theorem Units.mul_eq_one_iff_eq_inv {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} :
      a * u = 1 a = u⁻¹
      theorem AddUnits.add_eq_zero_iff_neg_eq {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α} :
      u + a = 0 ↑(-u) = a
      theorem Units.mul_eq_one_iff_inv_eq {α : Type u} [inst : Monoid α] {u : αˣ} {a : α} :
      u * a = 1 u⁻¹ = a
      theorem AddUnits.neg_unique {α : Type u} [inst : AddMonoid α] {u₁ : AddUnits α} {u₂ : AddUnits α} (h : u₁ = u₂) :
      ↑(-u₁) = ↑(-u₂)
      theorem Units.inv_unique {α : Type u} [inst : Monoid α] {u₁ : αˣ} {u₂ : αˣ} (h : u₁ = u₂) :
      u₁⁻¹ = u₂⁻¹
      @[simp]
      theorem AddUnits.val_neg_eq_neg_val {M : Type u_1} [inst : SubtractionMonoid M] (u : AddUnits M) :
      ↑(-u) = -u
      @[simp]
      theorem Units.val_inv_eq_inv_val {M : Type u_1} [inst : DivisionMonoid M] (u : Mˣ) :
      u⁻¹ = (u)⁻¹
      def AddUnits.mkOfAddEqZero.proof_1 {α : Type u_1} [inst : AddCommMonoid α] (a : α) (b : α) (hab : a + b = 0) :
      b + a = 0
      Equations
      • (_ : b + a = 0) = (_ : b + a = 0)
      def AddUnits.mkOfAddEqZero {α : Type u} [inst : AddCommMonoid α] (a : α) (b : α) (hab : a + b = 0) :

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

      Equations
      def Units.mkOfMulEqOne {α : Type u} [inst : 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
      @[simp]
      theorem AddUnits.val_mkOfAddEqZero {α : Type u} [inst : AddCommMonoid α] {a : α} {b : α} (h : a + b = 0) :
      @[simp]
      theorem Units.val_mkOfMulEqOne {α : Type u} [inst : CommMonoid α] {a : α} {b : α} (h : a * b = 1) :
      ↑(Units.mkOfMulEqOne a b h) = a
      def divp {α : Type u} [inst : Monoid α] (a : α) (u : αˣ) :
      α

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

      Equations

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

      Equations
      @[simp]
      theorem divp_self {α : Type u} [inst : Monoid α] (u : αˣ) :
      u /ₚ u = 1
      @[simp]
      theorem divp_one {α : Type u} [inst : Monoid α] (a : α) :
      a /ₚ 1 = a
      theorem divp_assoc {α : Type u} [inst : Monoid α] (a : α) (b : α) (u : αˣ) :
      a * b /ₚ u = a * (b /ₚ u)
      theorem divp_assoc' {α : Type u} [inst : 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} [inst : Monoid α] {a : α} (u : αˣ) :
      a /ₚ u⁻¹ = a * u
      @[simp]
      theorem divp_mul_cancel {α : Type u} [inst : Monoid α] (a : α) (u : αˣ) :
      a /ₚ u * u = a
      @[simp]
      theorem mul_divp_cancel {α : Type u} [inst : Monoid α] (a : α) (u : αˣ) :
      a * u /ₚ u = a
      @[simp]
      theorem divp_left_inj {α : Type u} [inst : Monoid α] (u : αˣ) {a : α} {b : α} :
      a /ₚ u = b /ₚ u a = b
      theorem divp_divp_eq_divp_mul {α : Type u} [inst : Monoid α] (x : α) (u₁ : αˣ) (u₂ : αˣ) :
      x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
      theorem divp_eq_iff_mul_eq {α : Type u} [inst : Monoid α] {x : α} {u : αˣ} {y : α} :
      x /ₚ u = y y * u = x
      theorem eq_divp_iff_mul_eq {α : Type u} [inst : Monoid α] {x : α} {u : αˣ} {y : α} :
      x = y /ₚ u x * u = y
      theorem divp_eq_one_iff_eq {α : Type u} [inst : Monoid α] {a : α} {u : αˣ} :
      a /ₚ u = 1 a = u
      @[simp]
      theorem one_divp {α : Type u} [inst : Monoid α] (u : αˣ) :
      1 /ₚ u = u⁻¹
      theorem inv_eq_one_divp {α : Type u} [inst : Monoid α] (u : αˣ) :
      u⁻¹ = 1 /ₚ u

      Used for field_simp to deal with inverses of units.

      theorem inv_eq_one_divp' {α : Type u} [inst : Monoid α] (u : αˣ) :
      ↑(1 / u) = 1 /ₚ u

      Used for field_simp to deal with inverses of units. This form of the lemma is essential since field_simp likes to use inv_eq_one_div to rewrite ↑u⁻¹ = ↑(1 / u)↑u⁻¹ = ↑(1 / u)⁻¹ = ↑(1 / u)↑(1 / u).

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

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

      theorem divp_mul_eq_mul_divp {α : Type u} [inst : CommMonoid α] (x : α) (y : α) (u : αˣ) :
      x /ₚ u * y = x * y /ₚ u
      theorem divp_eq_divp_iff {α : Type u} [inst : CommMonoid α] {x : α} {y : α} {ux : αˣ} {uy : αˣ} :
      x /ₚ ux = y /ₚ uy x * uy = y * ux
      theorem divp_mul_divp {α : Type u} [inst : CommMonoid α] (x : α) (y : α) (ux : αˣ) (uy : αˣ) :
      x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

      IsUnit predicate #

      def IsAddUnit {M : Type u_1} [inst : 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
      def IsUnit {M : Type u_1} [inst : 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
      theorem isAddUnit_of_subsingleton {M : Type u_1} [inst : AddMonoid M] [inst : Subsingleton M] (a : M) :
      theorem isUnit_of_subsingleton {M : Type u_1} [inst : Monoid M] [inst : Subsingleton M] (a : M) :
      instance instCanLiftAddUnitsValIsAddUnit {M : Type u_1} [inst : AddMonoid M] :
      CanLift M (AddUnits M) AddUnits.val IsAddUnit
      Equations
      def instCanLiftAddUnitsValIsAddUnit.proof_1 {M : Type u_1} [inst : AddMonoid M] :
      ∀ (x : M), IsAddUnit xIsAddUnit x
      Equations
      instance instCanLiftUnitsValIsUnit {M : Type u_1} [inst : Monoid M] :
      CanLift M Mˣ Units.val IsUnit
      Equations
      • instCanLiftUnitsValIsUnit = { prf := (_ : ∀ (x : M), IsUnit xIsUnit x) }
      def instUniqueAddUnits.proof_1 {M : Type u_1} [inst : AddMonoid M] [inst : Subsingleton M] (a : AddUnits M) :
      a = 0
      Equations
      • (_ : a = 0) = (_ : a = 0)
      instance instUniqueAddUnits {M : Type u_1} [inst : AddMonoid M] [inst : Subsingleton M] :

      A subsingleton AddMonoid has a unique additive unit.

      Equations
      • instUniqueAddUnits = { toInhabited := { default := 0 }, uniq := (_ : ∀ (a : AddUnits M), a = 0) }
      instance instUniqueUnits {M : Type u_1} [inst : Monoid M] [inst : Subsingleton M] :

      A subsingleton Monoid has a unique unit.

      Equations
      • instUniqueUnits = { toInhabited := { default := 1 }, uniq := (_ : ∀ (a : Mˣ), a = 1) }
      @[simp]
      theorem AddUnits.isAddUnit {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) :
      @[simp]
      theorem Units.isUnit {M : Type u_1} [inst : Monoid M] (u : Mˣ) :
      IsUnit u
      @[simp]
      theorem isAddUnit_zero {M : Type u_1} [inst : AddMonoid M] :
      @[simp]
      theorem isUnit_one {M : Type u_1} [inst : Monoid M] :
      theorem isAddUnit_of_add_eq_zero {M : Type u_1} [inst : AddCommMonoid M] (a : M) (b : M) (h : a + b = 0) :
      theorem isUnit_of_mul_eq_one {M : Type u_1} [inst : CommMonoid M] (a : M) (b : M) (h : a * b = 1) :
      theorem IsAddUnit.exists_neg {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) :
      b, a + b = 0
      theorem IsUnit.exists_right_inv {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) :
      b, a * b = 1
      theorem IsAddUnit.exists_neg' {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) :
      b, b + a = 0
      theorem IsUnit.exists_left_inv {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) :
      b, b * a = 1
      theorem isAddUnit_iff_exists_neg {M : Type u_1} [inst : AddCommMonoid M] {a : M} :
      IsAddUnit a b, a + b = 0
      abbrev isAddUnit_iff_exists_neg.match_1 {M : Type u_1} [inst : AddCommMonoid M] {a : M} (motive : (b, a + b = 0) → Prop) :
      (x : b, a + b = 0) → ((b : M) → (hab : a + b = 0) → motive (_ : b, a + b = 0)) → motive x
      Equations
      theorem isUnit_iff_exists_inv {M : Type u_1} [inst : CommMonoid M] {a : M} :
      IsUnit a b, a * b = 1
      theorem isAddUnit_iff_exists_neg' {M : Type u_1} [inst : AddCommMonoid M] {a : M} :
      IsAddUnit a b, b + a = 0
      theorem isUnit_iff_exists_inv' {M : Type u_1} [inst : CommMonoid M] {a : M} :
      IsUnit a b, b * a = 1
      theorem IsAddUnit.add {M : Type u_1} [inst : AddMonoid M] {x : M} {y : M} :
      IsAddUnit xIsAddUnit yIsAddUnit (x + y)
      theorem IsUnit.mul {M : Type u_1} [inst : Monoid M] {x : M} {y : M} :
      IsUnit xIsUnit yIsUnit (x * y)
      abbrev AddUnits.isAddUnit_add_addUnits.match_1 {M : Type u_1} [inst : AddMonoid M] (a : M) (u : AddUnits M) (motive : IsAddUnit (a + u)Prop) :
      (x : IsAddUnit (a + u)) → ((v : AddUnits M) → (hv : v = a + u) → motive (_ : u, u = a + u)) → motive x
      Equations
      @[simp]
      theorem AddUnits.isAddUnit_add_addUnits {M : Type u_1} [inst : AddMonoid M] (a : M) (u : AddUnits M) :

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

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

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

      abbrev AddUnits.isAddUnit_addUnits_add.match_1 {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) (motive : IsAddUnit (u + a)Prop) :
      (x : IsAddUnit (u + a)) → ((v : AddUnits M) → (hv : v = u + a) → motive (_ : u, u = u + a)) → motive x
      Equations
      @[simp]
      theorem AddUnits.isAddUnit_addUnits_add {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a : M) :

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

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

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

      abbrev isAddUnit_of_add_isAddUnit_left.match_1 {M : Type u_1} [inst : AddCommMonoid M] {x : M} {y : M} (motive : (b, x + y + b = 0) → Prop) :
      (x : b, x + y + b = 0) → ((z : M) → (hz : x + y + z = 0) → motive (_ : b, x + y + b = 0)) → motive x
      Equations
      theorem isAddUnit_of_add_isAddUnit_left {M : Type u_1} [inst : AddCommMonoid M] {x : M} {y : M} (hu : IsAddUnit (x + y)) :
      theorem isUnit_of_mul_isUnit_left {M : Type u_1} [inst : CommMonoid M] {x : M} {y : M} (hu : IsUnit (x * y)) :
      theorem isAddUnit_of_add_isAddUnit_right {M : Type u_1} [inst : AddCommMonoid M] {x : M} {y : M} (hu : IsAddUnit (x + y)) :
      theorem isUnit_of_mul_isUnit_right {M : Type u_1} [inst : CommMonoid M] {x : M} {y : M} (hu : IsUnit (x * y)) :
      @[simp]
      theorem IsAddUnit.add_iff {M : Type u_1} [inst : AddCommMonoid M] {x : M} {y : M} :
      @[simp]
      theorem IsUnit.mul_iff {M : Type u_1} [inst : CommMonoid M] {x : M} {y : M} :
      noncomputable def IsUnit.unit {M : Type u_1} [inst : 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
      noncomputable def IsAddUnit.addUnit {N : Type u_1} [inst : AddMonoid N] {a : N} (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
      @[simp]
      theorem IsAddUnit.addUnit_of_val_addUnits {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} (h : IsAddUnit a) :
      @[simp]
      theorem IsUnit.unit_of_val_units {M : Type u_1} [inst : Monoid M] {a : Mˣ} (h : IsUnit a) :
      @[simp]
      theorem IsAddUnit.addUnit_spec {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) :
      @[simp]
      theorem IsUnit.unit_spec {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) :
      ↑(IsUnit.unit h) = a
      @[simp]
      theorem IsAddUnit.val_neg_add {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) :
      @[simp]
      theorem IsUnit.val_inv_mul {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) :
      (IsUnit.unit h)⁻¹ * a = 1
      @[simp]
      theorem IsAddUnit.add_val_neg {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) :
      @[simp]
      theorem IsUnit.mul_val_inv {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) :
      a * (IsUnit.unit h)⁻¹ = 1
      instance IsAddUnit.instDecidableIsAddUnit {M : Type u_1} [inst : AddMonoid M] (x : M) [h : Decidable (u, u = x)] :

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

      Equations
      instance IsUnit.instDecidableIsUnit {M : Type u_1} [inst : Monoid M] (x : M) [h : Decidable (u, u = x)] :

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

      Equations
      abbrev IsAddUnit.add_left_inj.match_1 {M : Type u_1} [inst : AddMonoid M] {a : M} (motive : IsAddUnit aProp) :
      (h : IsAddUnit a) → ((u : AddUnits M) → (hu : u = a) → motive (_ : u, u = a)) → motive h
      Equations
      theorem IsAddUnit.add_left_inj {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit a) :
      b + a = c + a b = c
      theorem IsUnit.mul_left_inj {M : Type u_1} [inst : Monoid M] {a : M} {b : M} {c : M} (h : IsUnit a) :
      b * a = c * a b = c
      theorem IsAddUnit.add_right_inj {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit a) :
      a + b = a + c b = c
      theorem IsUnit.mul_right_inj {M : Type u_1} [inst : Monoid M] {a : M} {b : M} {c : M} (h : IsUnit a) :
      a * b = a * c b = c
      theorem IsAddUnit.add_left_cancel {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit a) :
      a + b = a + cb = c
      theorem IsUnit.mul_left_cancel {M : Type u_1} [inst : Monoid M] {a : M} {b : M} {c : M} (h : IsUnit a) :
      a * b = a * cb = c
      theorem IsAddUnit.add_right_cancel {M : Type u_1} [inst : AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit b) :
      a + b = c + ba = c
      theorem IsUnit.mul_right_cancel {M : Type u_1} [inst : Monoid M] {a : M} {b : M} {c : M} (h : IsUnit b) :
      a * b = c * ba = c
      theorem IsAddUnit.add_right_injective {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) :
      Function.Injective ((fun x x_1 => x + x_1) a)
      theorem IsUnit.mul_right_injective {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a) :
      Function.Injective ((fun x x_1 => x * x_1) a)
      theorem IsAddUnit.add_left_injective {M : Type u_1} [inst : AddMonoid M] {b : M} (h : IsAddUnit b) :
      Function.Injective fun x => x + b
      theorem IsUnit.mul_left_injective {M : Type u_1} [inst : Monoid M] {b : M} (h : IsUnit b) :
      Function.Injective fun x => x * b
      @[simp]
      theorem IsAddUnit.neg_add_cancel {M : Type u_1} [inst : SubtractionMonoid M] {a : M} :
      IsAddUnit a-a + a = 0
      @[simp]
      theorem IsUnit.inv_mul_cancel {M : Type u_1} [inst : DivisionMonoid M] {a : M} :
      IsUnit aa⁻¹ * a = 1
      @[simp]
      theorem IsAddUnit.add_neg_cancel {M : Type u_1} [inst : SubtractionMonoid M] {a : M} :
      IsAddUnit aa + -a = 0
      @[simp]
      theorem IsUnit.mul_inv_cancel {M : Type u_1} [inst : DivisionMonoid M] {a : M} :
      IsUnit aa * a⁻¹ = 1
      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
      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