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.

ink

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

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

ink

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 "ˣ")

ink

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

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

ink

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

ink

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

ink

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

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

Equations

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

ink

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 }

ink

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

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

ink

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

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

ink

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

ink

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

ink

theorem AddUnits.ext {α : Type u} [inst : AddMonoid α] : Function.Injective fun u => ↑u

ink

abbrev AddUnits.ext.match_1 {α : Type u_1} [inst : AddMonoid α] (motive : (x x_1 : AddUnits α) → (fun u => ↑u) x = (fun u => ↑u) x_1 → Prop) : (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.

ink

theorem Units.ext {α : Type u} [inst : Monoid α] : Function.Injective fun u => ↑u

ink

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

ink

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

ink

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

ink

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

ink

instance AddUnits.instDecidableEqAddUnits {α : Type u} [inst : AddMonoid α] [inst : 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)

ink

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

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

Equations

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

ink

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

ink

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

ink

def AddUnits.copy {α : Type u} [inst : 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) }

ink

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)

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

instance AddUnits.instAddZeroClassAddUnits {α : Type u} [inst : 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)

ink

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

Equations

• (_ : 0 + u = u) = (_ : 0 + u = u)

ink

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)

ink

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)

ink

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

Equations

• (_ : u + 0 = u) = (_ : u + 0 = u)

ink

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

Equations

• (_ : 0 + 0 = 0) = (_ : 0 + 0 = 0)

ink

instance Units.instMulOneClassUnits {α : Type u} [inst : 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)

ink

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

Equations

• (_ : -u + u = 0) = (_ : -u + u = 0)

ink

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

Equations

• (_ : ∀ (a : AddUnits α), 0 + a = a) = (_ : ∀ (a : AddUnits α), 0 + a = a)

ink

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

ink

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)

ink

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)

ink

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

Equations

• (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a) = (_ : zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a)

ink

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

Equations

• (_ : ∀ (a : AddUnits α), a + 0 = a) = (_ : ∀ (a : AddUnits α), a + 0 = a)

ink

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)

ink

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

ink

instance AddUnits.instAddGroupAddUnits {α : Type u} [inst : 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)

ink

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

• (_ : zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a) = (_ : zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a)

ink

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)

ink

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

Units of a monoid form a group.

Equations

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

ink

def AddUnits.instAddCommGroupAddUnitsToAddMonoid.proof_1 {α : Type u_1} [inst : AddCommMonoid α] (a : AddUnits α) : -a + a = 0

Equations

• (_ : ∀ (a : AddUnits α), -a + a = 0) = (_ : ∀ (a : AddUnits α), -a + a = 0)

ink

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)

ink

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

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)

ink

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

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)

ink

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

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

Equations

• AddUnits.instInhabitedAddUnits = { default := 0 }

ink

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

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

Equations

• Units.instInhabitedUnits = { default := 1 }

ink

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

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

Equations

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

ink

instance Units.instReprUnits {α : Type u} [inst : Monoid α] [inst : Repr α] : Repr αˣ

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

Equations

• Units.instReprUnits = { reprPrec := reprPrec ∘ Units.val }

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

theorem AddUnits.neg_eq_val_neg {α : Type u} [inst : AddMonoid α] (a : AddUnits α) : a.neg = ↑(-a)

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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)

ink

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

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

Equations

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

ink

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

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

ink

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

ink

@[simp]

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

ink

@[simp]

theorem divp_one {α : Type u} [inst : Monoid α] (a : α) : a /ₚ 1 = a

ink

theorem divp_assoc {α : Type u} [inst : Monoid α] (a : α) (b : α) (u : αˣ) : a * b /ₚ u = a * (b /ₚ u)

ink

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.

ink

@[simp]

theorem divp_inv {α : Type u} [inst : Monoid α] {a : α} (u : αˣ) : a /ₚ u⁻¹ = a * ↑u

ink

@[simp]

theorem divp_mul_cancel {α : Type u} [inst : Monoid α] (a : α) (u : αˣ) : a /ₚ u * ↑u = a

ink

@[simp]

theorem mul_divp_cancel {α : Type u} [inst : Monoid α] (a : α) (u : αˣ) : a * ↑u /ₚ u = a

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

theorem divp_eq_one_iff_eq {α : Type u} [inst : Monoid α] {a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = ↑u

ink

@[simp]

theorem one_divp {α : Type u} [inst : Monoid α] (u : αˣ) : 1 /ₚ u = ↑u⁻¹

ink

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

Used for field_simp to deal with inverses of units.

ink

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

ink

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

ink

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

ink

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

ink

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

IsUnit predicate

ink

def IsAddUnit {M : Type u_1} [inst : 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, ↑u = a

ink

def IsUnit {M : Type u_1} [inst : 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, ↑u = a

ink

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

ink

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

ink

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

Equations

• instCanLiftAddUnitsValIsAddUnit = { prf := (_ : ∀ (x : M), IsAddUnit x → IsAddUnit x) }

ink

def instCanLiftAddUnitsValIsAddUnit.proof_1 {M : Type u_1} [inst : AddMonoid M] : ∀ (x : M), IsAddUnit x → IsAddUnit x

Equations

• (_ : IsAddUnit x → IsAddUnit x) = (_ : IsAddUnit x → IsAddUnit x)

ink

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

Equations

• instCanLiftUnitsValIsUnit = { prf := (_ : ∀ (x : M), IsUnit x → IsUnit x) }

ink

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

Equations

• (_ : a = 0) = (_ : a = 0)

ink

instance instUniqueAddUnits {M : Type u_1} [inst : AddMonoid M] [inst : Subsingleton M] : Unique (AddUnits M)

A subsingleton AddMonoid has a unique additive unit.

Equations

• instUniqueAddUnits = { toInhabited := { default := 0 }, uniq := (_ : ∀ (a : AddUnits M), a = 0) }

ink

instance instUniqueUnits {M : Type u_1} [inst : Monoid M] [inst : Subsingleton M] : Unique Mˣ

A subsingleton Monoid has a unique unit.

Equations

• instUniqueUnits = { toInhabited := { default := 1 }, uniq := (_ : ∀ (a : Mˣ), a = 1) }

ink

@[simp]

theorem AddUnits.isAddUnit {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) : IsAddUnit ↑u

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

theorem IsAddUnit.exists_neg {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) : ∃ b, a + b = 0

ink

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

ink

theorem IsAddUnit.exists_neg' {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a) : ∃ b, b + a = 0

ink

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

ink

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

ink

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

• isAddUnit_iff_exists_neg.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

• AddUnits.isAddUnit_add_addUnits.match_1 a u motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

@[simp]

theorem AddUnits.isAddUnit_add_addUnits {M : Type u_1} [inst : 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.

ink

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

ink

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

• AddUnits.isAddUnit_addUnits_add.match_1 u a motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

@[simp]

theorem AddUnits.isAddUnit_addUnits_add {M : Type u_1} [inst : 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.

ink

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

ink

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

• isAddUnit_of_add_isAddUnit_left.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

noncomputable def IsUnit.unit {M : Type u_1} [inst : 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)⁻¹)

ink

noncomputable def IsAddUnit.addUnit {N : Type u_1} [inst : 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))

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

• IsAddUnit.instDecidableIsAddUnit x = h

ink

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

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

Equations

• IsUnit.instDecidableIsUnit x = h

ink

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

Equations

• IsAddUnit.add_left_inj.match_1 motive h h_1 = Exists.casesOn h fun w h => h_1 w h

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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)

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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 (h a))⁻¹ * a = 1)

ink

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)