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

• Units M: the group of units (i.e., invertible elements) of a monoid.
• IsUnit x: a predicate asserting that x is a unit (i.e., invertible element) of a monoid.

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

Notation

We provide Mˣ 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) [Monoid α] : Type u

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 : ↑s * s.inv = 1

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

• inv_val : s.inv * ↑s = 1

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

def «term_ˣ» : Lean.TrailingParserDescr

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

• «term_ˣ» = Lean.ParserDescr.trailingNode `term_ˣ 1024 1024 (Lean.ParserDescr.symbol "ˣ")

structure AddUnits (α : Type u) [AddMonoid α] : Type u

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.

• val : α

  The underlying value in the base AddMonoid.

• neg : α

  The additive inverse value of val in the base AddMonoid.

• val_neg : ↑s + s.neg = 0

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

• neg_val : s.neg + ↑s = 0

  neg is the left additive inverse of val in the base AddMonoid.

theorem unique_zero {α : Type u_1} [Unique α] [Zero α] : default = 0

theorem unique_one {α : Type u_1} [Unique α] [One α] : default = 1

instance AddUnits.instCoeHeadAddUnits {α : Type u} [AddMonoid α] : CoeHead (AddUnits α) α

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

Equations

• AddUnits.instCoeHeadAddUnits = { coe := AddUnits.val }

instance Units.instCoeHeadUnits {α : Type u} [Monoid α] : CoeHead αˣ α

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

Equations

• Units.instCoeHeadUnits = { coe := Units.val }

instance AddUnits.instNeg {α : Type u} [AddMonoid α] : Neg (AddUnits α)

The additive inverse of an additive unit in an AddMonoid.

Equations

• AddUnits.instNeg = { neg := fun (u : AddUnits α) => { val := u.neg, neg := ↑u, val_neg := (_ : u.neg + ↑u = 0), neg_val := (_ : ↑u + u.neg = 0) } }

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

The inverse of a unit in a Monoid.

Equations

• Units.instInv = { inv := fun (u : αˣ) => { val := u.inv, inv := ↑u, val_inv := (_ : u.inv * ↑u = 1), inv_val := (_ : ↑u * u.inv = 1) } }

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

See Note [custom simps projection]

Equations

• AddUnits.Simps.val_neg u = ↑(-u)

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

See Note [custom simps projection]

Equations

• Units.Simps.val_inv u = ↑u⁻¹

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.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

abbrev AddUnits.ext.match_1 {α : Type u_1} [AddMonoid α] (motive : (x x_1 : AddUnits α) → ↑x = ↑x_1 → Prop) : ∀ (x x_1 : AddUnits α) (x_2 : ↑x = ↑x_1), (∀ (v i₁ : α) (vi₁ : v + i₁ = 0) (iv₁ : i₁ + v = 0) (v' i₂ : α) (vi₂ : v' + i₂ = 0) (iv₂ : i₂ + v' = 0) (e : ↑{ val := v, neg := i₁, val_neg := vi₁, neg_val := iv₁ } = ↑{ 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

• (_ : motive x✝¹ x✝ x) = (_ : motive x✝¹ x✝ x)

theorem AddUnits.ext {α : Type u} [AddMonoid α] : Function.Injective AddUnits.val

theorem Units.ext {α : Type u} [Monoid α] : Function.Injective Units.val

theorem AddUnits.eq_iff {α : Type u} [AddMonoid α] {a : AddUnits α} {b : AddUnits α} : ↑a = ↑b ↔ a = b

theorem Units.eq_iff {α : Type u} [Monoid α] {a : αˣ} {b : αˣ} : ↑a = ↑b ↔ a = b

theorem AddUnits.ext_iff {α : Type u} [AddMonoid α] {a : AddUnits α} {b : AddUnits α} : a = b ↔ ↑a = ↑b

theorem Units.ext_iff {α : Type u} [Monoid α] {a : αˣ} {b : αˣ} : a = b ↔ ↑a = ↑b

instance AddUnits.instDecidableEqAddUnits {α : Type u} [AddMonoid α] [DecidableEq α] : DecidableEq (AddUnits α)

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

Equations

• AddUnits.instDecidableEqAddUnits x✝ x = decidable_of_iff' (↑x✝ = ↑x) (_ : x✝ = x ↔ ↑x✝ = ↑x)

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

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

Equations

• Units.instDecidableEqUnits x✝ x = decidable_of_iff' (↑x✝ = ↑x) (_ : x✝ = x ↔ ↑x✝ = ↑x)

@[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

@[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

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

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) }

theorem AddUnits.copy.proof_2 {α : Type u_1} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)) : inv + val = 0

theorem AddUnits.copy.proof_1 {α : Type u_1} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)) : val + inv = 0

@[simp]

theorem Units.val_copy {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹) : ↑(Units.copy u val hv inv hi) = val

@[simp]

theorem AddUnits.val_copy {α : Type u} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)) : ↑(AddUnits.copy u val hv inv hi) = val

@[simp]

theorem AddUnits.val_neg_copy {α : Type u} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)) : ↑(-AddUnits.copy u val hv inv hi) = inv

@[simp]

theorem Units.val_inv_copy {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹) : ↑(Units.copy u val hv inv hi)⁻¹ = inv

def Units.copy {α : Type u} [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} [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} [Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹) : Units.copy u val hv inv hi = u

instance AddUnits.instAddZeroClassAddUnits {α : Type u} [AddMonoid α] : AddZeroClass (AddUnits α)

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

Equations

• AddUnits.instAddZeroClassAddUnits = AddZeroClass.mk (_ : ∀ (u : AddUnits α), 0 + u = u) (_ : ∀ (u : AddUnits α), u + 0 = u)

theorem AddUnits.instAddZeroClassAddUnits.proof_1 {α : Type u_1} [AddMonoid α] : 0 + 0 = 0

theorem AddUnits.instAddZeroClassAddUnits.proof_3 {α : Type u_1} [AddMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) : u₂.neg + u₁.neg + (↑u₁ + ↑u₂) = 0

theorem AddUnits.instAddZeroClassAddUnits.proof_2 {α : Type u_1} [AddMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) : ↑u₁ + ↑u₂ + (u₂.neg + u₁.neg) = 0

theorem AddUnits.instAddZeroClassAddUnits.proof_5 {α : Type u_1} [AddMonoid α] (u : AddUnits α) : u + 0 = u

theorem AddUnits.instAddZeroClassAddUnits.proof_4 {α : Type u_1} [AddMonoid α] (u : AddUnits α) : 0 + u = u

instance Units.instMulOneClassUnits {α : Type u} [Monoid α] : MulOneClass αˣ

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

Equations

• Units.instMulOneClassUnits = MulOneClass.mk (_ : ∀ (u : αˣ), 1 * u = u) (_ : ∀ (u : αˣ), u * 1 = u)

theorem AddUnits.instAddGroupAddUnits.proof_1 {α : Type u_1} [AddMonoid α] : ∀ (x x_1 x_2 : AddUnits α), x + x_1 + x_2 = x + (x_1 + x_2)

theorem AddUnits.instAddGroupAddUnits.proof_7 {α : Type u_1} [AddMonoid α] : ∀ (a b : AddUnits α), a - b = a - b

theorem AddUnits.instAddGroupAddUnits.proof_9 {α : Type u_1} [AddMonoid α] : ∀ (n : ℕ) (a : AddUnits α), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

theorem AddUnits.instAddGroupAddUnits.proof_2 {α : Type u_1} [AddMonoid α] (a : AddUnits α) : 0 + a = a

theorem AddUnits.instAddGroupAddUnits.proof_5 {α : Type u_1} [AddMonoid α] : ∀ (n : ℕ) (x : AddUnits α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem AddUnits.instAddGroupAddUnits.proof_11 {α : Type u_1} [AddMonoid α] (u : AddUnits α) : -u + u = 0

theorem AddUnits.instAddGroupAddUnits.proof_6 {α : Type u_1} [AddMonoid α] : ∀ (x x_1 x_2 : AddUnits α), x + x_1 + x_2 = x + (x_1 + x_2)

theorem AddUnits.instAddGroupAddUnits.proof_8 {α : Type u_1} [AddMonoid α] : ∀ (a : AddUnits α), zsmulRec 0 a = zsmulRec 0 a

theorem AddUnits.instAddGroupAddUnits.proof_3 {α : Type u_1} [AddMonoid α] (a : AddUnits α) : a + 0 = a

theorem AddUnits.instAddGroupAddUnits.proof_4 {α : Type u_1} [AddMonoid α] : ∀ (x : AddUnits α), nsmulRec 0 x = nsmulRec 0 x

theorem AddUnits.instAddGroupAddUnits.proof_10 {α : Type u_1} [AddMonoid α] : ∀ (n : ℕ) (a : AddUnits α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

instance AddUnits.instAddGroupAddUnits {α : Type u} [AddMonoid α] : AddGroup (AddUnits α)

Additive units of an additive monoid form an additive group.

Equations

• AddUnits.instAddGroupAddUnits = let src := inferInstance; AddGroup.mk (_ : ∀ (u : AddUnits α), -u + u = 0)

instance Units.instGroupUnits {α : Type u} [Monoid α] : Group αˣ

Units of a monoid form a group.

Equations

• Units.instGroupUnits = let src := inferInstance; Group.mk (_ : ∀ (u : αˣ), u⁻¹ * u = 1)

instance AddUnits.instAddCommGroupAddUnits {α : Type u_1} [AddCommMonoid α] : AddCommGroup (AddUnits α)

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

Equations

• AddUnits.instAddCommGroupAddUnits = AddCommGroup.mk (_ : ∀ (x x_1 : AddUnits α), x + x_1 = x_1 + x)

theorem AddUnits.instAddCommGroupAddUnits.proof_1 {α : Type u_1} [AddCommMonoid α] : ∀ (x x_1 : AddUnits α), x + x_1 = x_1 + x

instance Units.instCommGroupUnits {α : Type u_1} [CommMonoid α] : CommGroup αˣ

Units of a commutative monoid form a commutative group.

Equations

• Units.instCommGroupUnits = CommGroup.mk (_ : ∀ (x x_1 : αˣ), x * x_1 = x_1 * x)

instance AddUnits.instInhabitedAddUnits {α : Type u} [AddMonoid α] : Inhabited (AddUnits α)

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

Equations

• AddUnits.instInhabitedAddUnits = { default := 0 }

instance Units.instInhabitedUnits {α : Type u} [Monoid α] : Inhabited αˣ

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

Equations

• Units.instInhabitedUnits = { default := 1 }

instance AddUnits.instReprAddUnits {α : Type u} [AddMonoid α] [Repr α] : Repr (AddUnits α)

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

Equations

• AddUnits.instReprAddUnits = { reprPrec := reprPrec ∘ AddUnits.val }

instance Units.instReprUnits {α : Type u} [Monoid α] [Repr α] : 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} [AddMonoid α] (a : AddUnits α) (b : AddUnits α) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem Units.val_mul {α : Type u} [Monoid α] (a : αˣ) (b : αˣ) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem AddUnits.val_zero {α : Type u} [AddMonoid α] : ↑0 = 0

@[simp]

theorem Units.val_one {α : Type u} [Monoid α] : ↑1 = 1

@[simp]

theorem AddUnits.val_eq_zero {α : Type u} [AddMonoid α] {a : AddUnits α} : ↑a = 0 ↔ a = 0

@[simp]

theorem Units.val_eq_one {α : Type u} [Monoid α] {a : αˣ} : ↑a = 1 ↔ a = 1

@[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_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_eq_val_neg {α : Type u} [AddMonoid α] (a : AddUnits α) : a.neg = ↑(-a)

@[simp]

theorem Units.inv_eq_val_inv {α : Type u} [Monoid α] (a : αˣ) : a.inv = ↑a⁻¹

@[simp]

theorem AddUnits.neg_add {α : Type u} [AddMonoid α] (a : AddUnits α) : ↑(-a) + ↑a = 0

@[simp]

theorem Units.inv_mul {α : Type u} [Monoid α] (a : αˣ) : ↑a⁻¹ * ↑a = 1

@[simp]

theorem AddUnits.add_neg {α : Type u} [AddMonoid α] (a : AddUnits α) : ↑a + ↑(-a) = 0

@[simp]

theorem Units.mul_inv {α : Type u} [Monoid α] (a : αˣ) : ↑a * ↑a⁻¹ = 1

theorem AddUnits.neg_add_of_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u = a) : ↑(-u) + a = 0

theorem Units.inv_mul_of_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1

theorem AddUnits.add_neg_of_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u = a) : a + ↑(-u) = 0

theorem Units.mul_inv_of_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1

@[simp]

theorem AddUnits.add_neg_cancel_left {α : Type u} [AddMonoid α] (a : AddUnits α) (b : α) : ↑a + (↑(-a) + b) = b

@[simp]

theorem Units.mul_inv_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

@[simp]

theorem Units.inv_mul_cancel_left {α : Type u} [Monoid α] (a : αˣ) (b : α) : ↑a⁻¹ * (↑a * b) = b

@[simp]

theorem AddUnits.add_neg_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) : a + ↑b + ↑(-b) = a

@[simp]

theorem Units.mul_inv_cancel_right {α : Type u} [Monoid α] (a : α) (b : αˣ) : a * ↑b * ↑b⁻¹ = a

@[simp]

theorem AddUnits.neg_add_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) : a + ↑(-b) + ↑b = a

@[simp]

theorem Units.inv_mul_cancel_right {α : Type u} [Monoid α] (a : α) (b : αˣ) : a * ↑b⁻¹ * ↑b = a

@[simp]

theorem AddUnits.add_right_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b : α} {c : α} : ↑a + b = ↑a + c ↔ b = c

@[simp]

theorem Units.mul_right_inj {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} : ↑a * b = ↑a * c ↔ b = c

@[simp]

theorem AddUnits.add_left_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b : α} {c : α} : b + ↑a = c + ↑a ↔ b = c

@[simp]

theorem Units.mul_left_inj {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} : b * ↑a = c * ↑a ↔ b = c

theorem AddUnits.eq_add_neg_iff_add_eq {α : Type u} [AddMonoid α] (c : AddUnits α) {a : α} {b : α} : a = b + ↑(-c) ↔ a + ↑c = b

theorem Units.eq_mul_inv_iff_mul_eq {α : Type u} [Monoid α] (c : αˣ) {a : α} {b : α} : a = b * ↑c⁻¹ ↔ a * ↑c = b

theorem AddUnits.eq_neg_add_iff_add_eq {α : Type u} [AddMonoid α] (b : AddUnits α) {a : α} {c : α} : a = ↑(-b) + c ↔ ↑b + a = c

theorem Units.eq_inv_mul_iff_mul_eq {α : Type u} [Monoid α] (b : αˣ) {a : α} {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

theorem Units.inv_mul_eq_iff_eq_mul {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} : ↑a⁻¹ * b = c ↔ b = ↑a * c

theorem AddUnits.add_neg_eq_iff_eq_add {α : Type u} [AddMonoid α] (b : AddUnits α) {a : α} {c : α} : a + ↑(-b) = c ↔ a = c + ↑b

theorem Units.mul_inv_eq_iff_eq_mul {α : Type u} [Monoid α] (b : αˣ) {a : α} {c : α} : a * ↑b⁻¹ = c ↔ a = c * ↑b

theorem AddUnits.neg_eq_of_add_eq_zero_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 0) : ↑(-u) = a

theorem Units.inv_eq_of_mul_eq_one_left {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) : ↑u⁻¹ = a

theorem AddUnits.neg_eq_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) : ↑(-u) = a

theorem Units.inv_eq_of_mul_eq_one_right {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a

theorem AddUnits.eq_neg_of_add_eq_zero_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) : a = ↑(-u)

theorem Units.eq_inv_of_mul_eq_one_left {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) : a = ↑u⁻¹

theorem AddUnits.eq_neg_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 0) : a = ↑(-u)

theorem Units.eq_inv_of_mul_eq_one_right {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) : a = ↑u⁻¹

@[simp]

theorem AddUnits.add_neg_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : a + ↑(-u) = 0 ↔ a = ↑u

@[simp]

theorem Units.mul_inv_eq_one {α : Type u} [Monoid α] {u : αˣ} {a : α} : a * ↑u⁻¹ = 1 ↔ a = ↑u

@[simp]

theorem AddUnits.neg_add_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : ↑(-u) + a = 0 ↔ ↑u = a

@[simp]

theorem Units.inv_mul_eq_one {α : Type u} [Monoid α] {u : αˣ} {a : α} : ↑u⁻¹ * a = 1 ↔ ↑u = a

theorem AddUnits.add_eq_zero_iff_eq_neg {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : a + ↑u = 0 ↔ a = ↑(-u)

theorem Units.mul_eq_one_iff_eq_inv {α : Type u} [Monoid α] {u : αˣ} {a : α} : a * ↑u = 1 ↔ a = ↑u⁻¹

theorem AddUnits.add_eq_zero_iff_neg_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : ↑u + a = 0 ↔ ↑(-u) = a

theorem Units.mul_eq_one_iff_inv_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a

theorem AddUnits.neg_unique {α : Type u} [AddMonoid α] {u₁ : AddUnits α} {u₂ : AddUnits α} (h : ↑u₁ = ↑u₂) : ↑(-u₁) = ↑(-u₂)

theorem Units.inv_unique {α : Type u} [Monoid α] {u₁ : αˣ} {u₂ : αˣ} (h : ↑u₁ = ↑u₂) : ↑u₁⁻¹ = ↑u₂⁻¹

@[simp]

theorem AddUnits.val_neg_eq_neg_val {M : Type u_1} [SubtractionMonoid M] (u : AddUnits M) : ↑(-u) = -↑u

@[simp]

theorem Units.val_inv_eq_inv_val {M : Type u_1} [DivisionMonoid M] (u : Mˣ) : ↑u⁻¹ = (↑u)⁻¹

theorem AddUnits.mkOfAddEqZero.proof_1 {α : Type u_1} [AddCommMonoid α] (a : α) (b : α) (hab : a + b = 0) : b + a = 0

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

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

Equations

• AddUnits.mkOfAddEqZero a b hab = { val := a, neg := b, val_neg := hab, neg_val := (_ : b + a = 0) }

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

• Units.mkOfMulEqOne a b hab = { val := a, inv := b, val_inv := hab, inv_val := (_ : b * a = 1) }

@[simp]

theorem AddUnits.val_mkOfAddEqZero {α : Type u} [AddCommMonoid α] {a : α} {b : α} (h : a + b = 0) : ↑(AddUnits.mkOfAddEqZero a b h) = a

@[simp]

theorem Units.val_mkOfMulEqOne {α : Type u} [CommMonoid α] {a : α} {b : α} (h : a * b = 1) : ↑(Units.mkOfMulEqOne a b h) = a

def divp {α : Type u} [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

• a /ₚ u = a * ↑u⁻¹

def «term_/ₚ_» : Lean.TrailingParserDescr

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

• «term_/ₚ_» = Lean.ParserDescr.trailingNode `term_/ₚ_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ₚ ") (Lean.ParserDescr.cat `term 71))

@[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

@[simp]

theorem divp_left_inj {α : Type u} [Monoid α] (u : αˣ) {a : α} {b : α} : a /ₚ u = b /ₚ u ↔ a = b

theorem divp_divp_eq_divp_mul {α : Type u} [Monoid α] (x : α) (u₁ : αˣ) (u₂ : αˣ) : x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

theorem divp_eq_iff_mul_eq {α : Type u} [Monoid α] {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * ↑u = x

theorem eq_divp_iff_mul_eq {α : Type u} [Monoid α] {x : α} {u : αˣ} {y : α} : x = y /ₚ u ↔ x * ↑u = y

theorem divp_eq_one_iff_eq {α : Type u} [Monoid α] {a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = ↑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 inv_eq_one_divp' {α : Type u} [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).

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 α.

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

theorem divp_eq_divp_iff {α : Type u} [CommMonoid α] {x : α} {y : α} {ux : αˣ} {uy : αˣ} : x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux

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

theorem eq_zero_of_add_right {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} (h : a + b = 0) : a = 0

theorem eq_one_of_mul_right {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} (h : a * b = 1) : a = 1

theorem eq_zero_of_add_left {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} (h : a + b = 0) : b = 0

theorem eq_one_of_mul_left {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} (h : a * b = 1) : b = 1

@[simp]

theorem add_eq_zero {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} : a + b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem mul_eq_one {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} : a * b = 1 ↔ a = 1 ∧ b = 1

IsUnit predicate

def IsAddUnit {M : Type u_1} [AddMonoid M] (a : M) : Prop

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

• IsAddUnit a = ∃ (u : AddUnits M), ↑u = a

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

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 Mˣ is a bundled version of IsUnit.

Equations

• IsUnit a = ∃ (u : Mˣ), ↑u = a

theorem isAddUnit_of_subsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] (a : M) : IsAddUnit a

theorem isUnit_of_subsingleton {M : Type u_1} [Monoid M] [Subsingleton M] (a : M) : IsUnit a

instance instCanLiftAddUnitsValIsAddUnit {M : Type u_1} [AddMonoid M] : CanLift M (AddUnits M) AddUnits.val IsAddUnit

Equations

• (_ : CanLift M (AddUnits M) AddUnits.val IsAddUnit) = (_ : CanLift M (AddUnits M) AddUnits.val IsAddUnit)

instance instCanLiftUnitsValIsUnit {M : Type u_1} [Monoid M] : CanLift M Mˣ Units.val IsUnit

Equations

• (_ : CanLift M Mˣ Units.val IsUnit) = (_ : CanLift M Mˣ Units.val IsUnit)

theorem instUniqueAddUnits.proof_1 {M : Type u_1} [AddMonoid M] [Subsingleton M] (a : AddUnits M) : a = 0

instance instUniqueAddUnits {M : Type u_1} [AddMonoid M] [Subsingleton M] : Unique (AddUnits 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} [Monoid M] [Subsingleton M] : Unique 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} [AddMonoid M] (u : AddUnits M) : IsAddUnit ↑u

@[simp]

theorem Units.isUnit {M : Type u_1} [Monoid M] (u : Mˣ) : IsUnit ↑u

@[simp]

theorem isAddUnit_zero {M : Type u_1} [AddMonoid M] : IsAddUnit 0

@[simp]

theorem isUnit_one {M : Type u_1} [Monoid M] : IsUnit 1

theorem isAddUnit_of_add_eq_zero {M : Type u_1} [AddCommMonoid M] (a : M) (b : M) (h : a + b = 0) : IsAddUnit a

theorem isUnit_of_mul_eq_one {M : Type u_1} [CommMonoid M] (a : M) (b : M) (h : a * b = 1) : IsUnit a

theorem IsAddUnit.exists_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : ∃ (b : M), 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), b + a = 0

theorem IsUnit.exists_left_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : ∃ (b : M), b * a = 1

theorem isAddUnit_iff_exists_neg {M : Type u_1} [AddCommMonoid M] {a : M} : IsAddUnit a ↔ ∃ (b : M), a + b = 0

abbrev isAddUnit_iff_exists_neg.match_1 {M : Type u_1} [AddCommMonoid M] {a : M} (motive : (∃ (b : M), a + b = 0) → Prop) : ∀ (x : ∃ (b : M), a + b = 0), (∀ (b : M) (hab : a + b = 0), motive (_ : ∃ (b : M), a + b = 0)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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), b + a = 0

theorem isUnit_iff_exists_inv' {M : Type u_1} [CommMonoid M] {a : M} : IsUnit a ↔ ∃ (b : M), b * a = 1

theorem IsAddUnit.add {M : Type u_1} [AddMonoid M] {x : M} {y : M} : IsAddUnit x → IsAddUnit y → IsAddUnit (x + y)

theorem IsUnit.mul {M : Type u_1} [Monoid M] {x : M} {y : M} : IsUnit x → IsUnit y → IsUnit (x * y)

@[simp]

theorem AddUnits.isAddUnit_add_addUnits {M : Type u_1} [AddMonoid M] (a : M) (u : AddUnits M) : IsAddUnit (a + ↑u) ↔ IsAddUnit a

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

abbrev AddUnits.isAddUnit_add_addUnits.match_1 {M : Type u_1} [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_1 : AddUnits M), ↑u_1 = a + ↑u)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

@[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.

abbrev AddUnits.isAddUnit_addUnits_add.match_1 {M : Type u_1} [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_1 : AddUnits M), ↑u_1 = ↑u + a)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

@[simp]

theorem AddUnits.isAddUnit_addUnits_add {M : Type u_3} [AddMonoid M] (u : AddUnits M) (a : M) : IsAddUnit (↑u + a) ↔ IsAddUnit a

Addition of a u : AddUnits M on the left 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.

theorem isAddUnit_of_add_isAddUnit_left {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} (hu : IsAddUnit (x + y)) : IsAddUnit x

abbrev isAddUnit_of_add_isAddUnit_left.match_1 {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} (motive : (∃ (b : M), x + y + b = 0) → Prop) : ∀ (x_1 : ∃ (b : M), x + y + b = 0), (∀ (z : M) (hz : x + y + z = 0), motive (_ : ∃ (b : M), x + y + b = 0)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem isUnit_of_mul_isUnit_left {M : Type u_1} [CommMonoid M] {x : M} {y : M} (hu : IsUnit (x * y)) : IsUnit x

theorem isAddUnit_of_add_isAddUnit_right {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} (hu : IsAddUnit (x + y)) : IsAddUnit y

theorem isUnit_of_mul_isUnit_right {M : Type u_1} [CommMonoid M] {x : M} {y : M} (hu : IsUnit (x * y)) : IsUnit y

@[simp]

theorem IsAddUnit.add_iff {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} : IsAddUnit (x + y) ↔ IsAddUnit x ∧ IsAddUnit y

@[simp]

theorem IsUnit.mul_iff {M : Type u_1} [CommMonoid M] {x : M} {y : M} : IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y

noncomputable def IsUnit.unit {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : Mˣ

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

• IsUnit.unit h = Units.copy (Classical.choose h) a (_ : a = ↑(Classical.choose h)) ↑(Classical.choose h)⁻¹ (_ : ↑(Classical.choose h)⁻¹ = ↑(Classical.choose h)⁻¹)

noncomputable def IsAddUnit.addUnit {N : Type u_2} [AddMonoid N] {a : N} (h : IsAddUnit a) : AddUnits N

"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

• IsAddUnit.addUnit h = AddUnits.copy (Classical.choose h) a (_ : a = ↑(Classical.choose h)) ↑(-Classical.choose h) (_ : ↑(-Classical.choose h) = ↑(-Classical.choose h))

@[simp]

theorem IsAddUnit.addUnit_of_val_addUnits {M : Type u_1} [AddMonoid M] {a : AddUnits M} (h : IsAddUnit ↑a) : IsAddUnit.addUnit h = a

@[simp]

theorem IsUnit.unit_of_val_units {M : Type u_1} [Monoid M] {a : Mˣ} (h : IsUnit ↑a) : IsUnit.unit h = a

@[simp]

theorem IsAddUnit.addUnit_spec {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : ↑(IsAddUnit.addUnit h) = a

@[simp]

theorem IsUnit.unit_spec {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : ↑(IsUnit.unit h) = a

@[simp]

theorem IsAddUnit.val_neg_add {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : ↑(-IsAddUnit.addUnit h) + a = 0

@[simp]

theorem IsUnit.val_inv_mul {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : ↑(IsUnit.unit h)⁻¹ * a = 1

@[simp]

theorem IsAddUnit.add_val_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : a + ↑(-IsAddUnit.addUnit h) = 0

@[simp]

theorem IsUnit.mul_val_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : a * ↑(IsUnit.unit h)⁻¹ = 1

instance IsAddUnit.instDecidableIsAddUnit {M : Type u_1} [AddMonoid M] (x : M) [h : Decidable (∃ (u : AddUnits M), ↑u = x)] : Decidable (IsAddUnit x)

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

Equations

• IsAddUnit.instDecidableIsAddUnit x = h

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

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

Equations

• IsUnit.instDecidableIsUnit x = h

theorem IsAddUnit.add_left_inj {M : Type u_1} [AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit a) : b + a = c + a ↔ b = c

abbrev IsAddUnit.add_left_inj.match_1 {M : Type u_1} [AddMonoid M] {a : M} (motive : IsAddUnit a → Prop) : ∀ (h : IsAddUnit a), (∀ (u : AddUnits M) (hu : ↑u = a), motive (_ : ∃ (u : AddUnits M), ↑u = a)) → motive h

Equations

• (_ : motive h) = (_ : motive h)

theorem IsUnit.mul_left_inj {M : Type u_1} [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} [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} [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} [AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit a) : a + b = a + c → b = c

theorem IsUnit.mul_left_cancel {M : Type u_1} [Monoid M] {a : M} {b : M} {c : M} (h : IsUnit a) : a * b = a * c → b = c

theorem IsAddUnit.add_right_cancel {M : Type u_1} [AddMonoid M] {a : M} {b : M} {c : M} (h : IsAddUnit b) : a + b = c + b → a = c

theorem IsUnit.mul_right_cancel {M : Type u_1} [Monoid M] {a : M} {b : M} {c : M} (h : IsUnit b) : a * b = c * b → a = c

theorem IsAddUnit.add_right_injective {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : Function.Injective ((fun (x x_1 : M) => x + x_1) a)

theorem IsUnit.mul_right_injective {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : Function.Injective ((fun (x x_1 : M) => x * x_1) a)

theorem IsAddUnit.add_left_injective {M : Type u_1} [AddMonoid M] {b : M} (h : IsAddUnit b) : Function.Injective fun (x : M) => x + b

theorem IsUnit.mul_left_injective {M : Type u_1} [Monoid M] {b : M} (h : IsUnit b) : Function.Injective fun (x : M) => x * b

@[simp]

theorem IsAddUnit.neg_add_cancel {M : Type u_1} [SubtractionMonoid M] {a : M} : IsAddUnit a → -a + a = 0

@[simp]

theorem IsUnit.inv_mul_cancel {M : Type u_1} [DivisionMonoid M] {a : M} : IsUnit a → a⁻¹ * a = 1

@[simp]

theorem IsAddUnit.add_neg_cancel {M : Type u_1} [SubtractionMonoid M] {a : M} : IsAddUnit a → a + -a = 0

@[simp]

theorem IsUnit.mul_inv_cancel {M : Type u_1} [DivisionMonoid M] {a : M} : IsUnit a → a * a⁻¹ = 1

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

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

Equations

• groupOfIsUnit h = Group.mk (_ : ∀ (a : M), ↑(IsUnit.unit (_ : IsUnit a))⁻¹ * a = 1)

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

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

Equations

• commGroupOfIsUnit h = CommGroup.mk (_ : ∀ (a b : M), a * b = b * a)