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.

TODO #

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

source

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 : ↑self * self.inv = 1
inv is the right inverse of val in the base Monoid.
inv_val : self.inv * ↑self = 1
inv is the left inverse of val in the base Monoid.

Instances For

source

theorem Units.val_inv {α : Type u} [Monoid α] (self : αˣ) :

↑self * self.inv = 1

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

source

theorem Units.inv_val {α : Type u} [Monoid α] (self : αˣ) :

self.inv * ↑self = 1

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

source

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

source

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 : ↑self + self.neg = 0
neg is the right additive inverse of val in the base AddMonoid.
neg_val : self.neg + ↑self = 0
neg is the left additive inverse of val in the base AddMonoid.

Instances For

source

theorem AddUnits.val_neg {α : Type u} [AddMonoid α] (self : AddUnits α) :

↑self + self.neg = 0

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

source

theorem AddUnits.neg_val {α : Type u} [AddMonoid α] (self : AddUnits α) :

self.neg + ↑self = 0

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

source

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

CoeHead αˣ α

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

Equations

Units.instCoeHead = { coe := Units.val }

source

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

CoeHead (AddUnits α) α

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

Equations

AddUnits.instCoeHead = { coe := AddUnits.val }

source

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 := ⋯, inv_val := ⋯ } }

source

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 := ⋯, neg_val := ⋯ } }

source

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

See Note [custom simps projection]

Equations

Units.Simps.val_inv u = ↑u⁻¹

source

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

See Note [custom simps projection]

Equations

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

source

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

source

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

source

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

Function.Injective AddUnits.val

source

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

Function.Injective Units.val

source

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

↑a = ↑b ↔ a = b

source

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

↑a = ↑b ↔ a = b

source

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

DecidableEq αˣ

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

Equations

x✝.instDecidableEq x = decidable_of_iff' (↑x✝ = ↑x) ⋯

source

instance AddUnits.instDecidableEq {α : Type u} [AddMonoid α] [DecidableEq α] :

DecidableEq (AddUnits α)

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

Equations

x✝.instDecidableEq x = decidable_of_iff' (↑x✝ = ↑x) ⋯

source

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

source

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

source

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

αˣ

Copy a unit, adjusting definition equalities.

Equations

u.copy val hv inv hi = { val := val, inv := inv, val_inv := ⋯, inv_val := ⋯ }

source

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

AddUnits α

Copy an AddUnit, adjusting definitional equalities.

Equations

u.copy val hv inv hi = { val := val, neg := inv, val_neg := ⋯, neg_val := ⋯ }

source

@[simp]

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

↑(-u.copy val hv inv hi) = inv

source

@[simp]

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

↑(u.copy val hv inv hi) = val

source

@[simp]

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

↑(u.copy val hv inv hi) = val

source

@[simp]

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

↑(u.copy val hv inv hi)⁻¹ = inv

source

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

u.copy val hv inv hi = u

source

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

u.copy val hv inv hi = u

source

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

Mul αˣ

Units of a monoid have an induced multiplication.

Equations

Units.instMul = { mul := fun (u₁ u₂ : αˣ) => { val := ↑u₁ * ↑u₂, inv := u₂.inv * u₁.inv, val_inv := ⋯, inv_val := ⋯ } }

source

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

Add (AddUnits α)

Additive units of an additive monoid have an induced addition.

Equations

AddUnits.instAdd = { add := fun (u₁ u₂ : AddUnits α) => { val := ↑u₁ + ↑u₂, neg := u₂.neg + u₁.neg, val_neg := ⋯, neg_val := ⋯ } }

source

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

One αˣ

Units of a monoid have a unit

Equations

Units.instOne = { one := { val := 1, inv := 1, val_inv := ⋯, inv_val := ⋯ } }

source

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

Zero (AddUnits α)

Additive units of an additive monoid have a zero.

Equations

AddUnits.instZero = { zero := { val := 0, neg := 0, val_neg := ⋯, neg_val := ⋯ } }

source

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

MulOneClass αˣ

Units of a monoid have a multiplication and multiplicative identity.

Equations

Units.instMulOneClass = MulOneClass.mk ⋯ ⋯

source

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

AddZeroClass (AddUnits α)

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

Equations

AddUnits.instAddZeroClass = AddZeroClass.mk ⋯ ⋯

source

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

Inhabited αˣ

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

Equations

Units.instInhabited = { default := 1 }

source

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

Inhabited (AddUnits α)

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

Equations

AddUnits.instInhabited = { default := 0 }

source

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

Repr αˣ

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

Equations

Units.instRepr = { reprPrec := reprPrec ∘ Units.val }

source

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

Repr (AddUnits α)

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

Equations

AddUnits.instRepr = { reprPrec := reprPrec ∘ AddUnits.val }

source

@[simp]

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

↑(a * b) = ↑a * ↑b

source

@[simp]

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

↑(a + b) = ↑a + ↑b

source

@[simp]

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

↑1 = 1

source

@[simp]

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

↑0 = 0

source

@[simp]

theorem Units.val_eq_one {α : Type u} [Monoid α] {a : αˣ} :

↑a = 1 ↔ a = 1

source

@[simp]

theorem AddUnits.val_eq_zero {α : Type u} [AddMonoid α] {a : AddUnits α} :

↑a = 0 ↔ a = 0

source

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

source

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

source

@[simp]

theorem Units.inv_eq_val_inv {α : Type u} [Monoid α] (a : αˣ) :

a.inv = ↑a⁻¹

source

@[simp]

theorem AddUnits.neg_eq_val_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :

a.neg = ↑(-a)

source

@[simp]

theorem Units.inv_mul {α : Type u} [Monoid α] (a : αˣ) :

↑a⁻¹ * ↑a = 1

source

@[simp]

theorem AddUnits.neg_add {α : Type u} [AddMonoid α] (a : AddUnits α) :

↑(-a) + ↑a = 0

source

@[simp]

theorem Units.mul_inv {α : Type u} [Monoid α] (a : αˣ) :

↑a * ↑a⁻¹ = 1

source

@[simp]

theorem AddUnits.add_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :

↑a + ↑(-a) = 0

source

theorem Units.commute_coe_inv {α : Type u} [Monoid α] (a : αˣ) :

Commute ↑a ↑a⁻¹

source

theorem AddUnits.addCommute_coe_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :

AddCommute ↑a ↑(-a)

source

theorem Units.commute_inv_coe {α : Type u} [Monoid α] (a : αˣ) :

Commute ↑a⁻¹ ↑a

source

theorem AddUnits.addCommute_neg_coe {α : Type u} [AddMonoid α] (a : AddUnits α) :

AddCommute ↑(-a) ↑a

source

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

↑u⁻¹ * a = 1

source

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

↑(-u) + a = 0

source

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

a * ↑u⁻¹ = 1

source

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

a + ↑(-u) = 0

source

@[simp]

theorem Units.mul_inv_cancel_left {α : Type u} [Monoid α] (a : αˣ) (b : α) :

↑a * (↑a⁻¹ * b) = b

source

@[simp]

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

↑a + (↑(-a) + b) = b

source

@[simp]

theorem Units.inv_mul_cancel_left {α : Type u} [Monoid α] (a : αˣ) (b : α) :

↑a⁻¹ * (↑a * b) = b

source

@[simp]

theorem AddUnits.neg_add_cancel_left {α : Type u} [AddMonoid α] (a : AddUnits α) (b : α) :

↑(-a) + (↑a + b) = b

source

theorem Units.inv_mul_eq_iff_eq_mul {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} :

↑a⁻¹ * b = c ↔ b = ↑a * c

source

theorem AddUnits.neg_add_eq_iff_eq_add {α : Type u} [AddMonoid α] (a : AddUnits α) {b : α} {c : α} :

↑(-a) + b = c ↔ b = ↑a + c

source

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

Monoid αˣ

Equations

Units.instMonoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (a : αˣ) => { val := ↑a ^ n, inv := ↑a⁻¹ ^ n, val_inv := ⋯, inv_val := ⋯ }) ⋯ ⋯

source

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

AddMonoid (AddUnits α)

Equations

AddUnits.instAddMonoid = AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (a : AddUnits α) => { val := n • ↑a, neg := n • ↑(-a), val_neg := ⋯, neg_val := ⋯ }) ⋯ ⋯

source

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

Div αˣ

Units of a monoid have division

Equations

Units.instDiv = { div := fun (a b : αˣ) => { val := ↑a * ↑b⁻¹, inv := ↑b * ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } }

source

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

Sub (AddUnits α)

Additive units of an additive monoid have subtraction.

Equations

AddUnits.instSub = { sub := fun (a b : AddUnits α) => { val := ↑a + ↑(-b), neg := ↑b + ↑(-a), val_neg := ⋯, neg_val := ⋯ } }

source

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

DivInvMonoid αˣ

Units of a monoid form a DivInvMonoid.

Equations

Units.instDivInvMonoid = DivInvMonoid.mk ⋯ (fun (n : ℤ) (a : αˣ) => match n, a with | Int.ofNat n, a => a ^ n | Int.negSucc n, a => (a ^ n.succ)⁻¹) ⋯ ⋯ ⋯

source

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

SubNegMonoid (AddUnits α)

Additive units of an additive monoid form a SubNegMonoid.

Equations

AddUnits.instSubNegAddMonoid = SubNegMonoid.mk ⋯ (fun (n : ℤ) (a : AddUnits α) => match n, a with | Int.ofNat n, a => n • a | Int.negSucc n, a => -(n.succ • a)) ⋯ ⋯ ⋯

source

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

Group αˣ

Units of a monoid form a group.

Equations

Units.instGroup = Group.mk ⋯

source

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

AddGroup (AddUnits α)

Additive units of an additive monoid form an additive group.

Equations

AddUnits.instAddGroup = AddGroup.mk ⋯

source

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

CommGroup αˣ

Units of a commutative monoid form a commutative group.

Equations

Units.instCommGroupUnits = CommGroup.mk ⋯

source

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 ⋯

source

@[simp]

theorem Units.val_pow_eq_pow_val {α : Type u} [Monoid α] (a : αˣ) (n : ℕ) :

↑(a ^ n) = ↑a ^ n

source

@[simp]

theorem AddUnits.val_nsmul_eq_nsmul_val {α : Type u} [AddMonoid α] (a : AddUnits α) (n : ℕ) :

↑(n • a) = n • ↑a

source

@[simp]

theorem Units.val_inv_eq_inv_val {α : Type u} [DivisionMonoid α] (u : αˣ) :

↑u⁻¹ = (↑u)⁻¹

source

@[simp]

theorem AddUnits.val_neg_eq_neg_val {α : Type u} [SubtractionMonoid α] (u : AddUnits α) :

↑(-u) = -↑u

source

@[simp]

theorem Units.val_div_eq_div_val {α : Type u} [DivisionMonoid α] (u₁ : αˣ) (u₂ : αˣ) :

↑(u₁ / u₂) = ↑u₁ / ↑u₂

source

@[simp]

theorem AddUnits.val_sub_eq_sub_val {α : Type u} [SubtractionMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :

↑(u₁ - u₂) = ↑u₁ - ↑u₂

source

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 := ⋯ }

source

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 := ⋯ }

source

@[simp]

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

↑(Units.mkOfMulEqOne a b h) = a

source

@[simp]

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

↑(AddUnits.mkOfAddEqZero a b h) = a

source

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⁻¹

source

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

source

@[simp]

theorem divp_self {α : Type u} [Monoid α] (u : αˣ) :

↑u /ₚ u = 1

source

@[simp]

theorem divp_one {α : Type u} [Monoid α] (a : α) :

a /ₚ 1 = a

source

theorem divp_assoc {α : Type u} [Monoid α] (a : α) (b : α) (u : αˣ) :

a * b /ₚ u = a * (b /ₚ u)

source

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.

source

@[simp]

theorem divp_inv {α : Type u} [Monoid α] {a : α} (u : αˣ) :

a /ₚ u⁻¹ = a * ↑u

source

@[simp]

theorem divp_mul_cancel {α : Type u} [Monoid α] (a : α) (u : αˣ) :

a /ₚ u * ↑u = a

source

@[simp]

theorem mul_divp_cancel {α : Type u} [Monoid α] (a : α) (u : αˣ) :

a * ↑u /ₚ u = a

source

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

x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)

source

@[simp]

theorem one_divp {α : Type u} [Monoid α] (u : αˣ) :

1 /ₚ u = ↑u⁻¹

source

theorem inv_eq_one_divp {α : Type u} [Monoid α] (u : αˣ) :

↑u⁻¹ = 1 /ₚ u

Used for field_simp to deal with inverses of units.

source

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

↑(u₁ / u₂) = ↑u₁ /ₚ u₂

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

`IsUnit` predicate #

source

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

Instances For

source

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

Instances For

source

theorem isUnit_iff_exists {M : Type u_1} [Monoid M] {x : M} :

IsUnit x ↔ ∃ (b : M), x * b = 1 ∧ b * x = 1

See isUnit_iff_exists_and_exists for a similar lemma with two existentials.

source

theorem isAddUnit_iff_exists {M : Type u_1} [AddMonoid M] {x : M} :

IsAddUnit x ↔ ∃ (b : M), x + b = 0 ∧ b + x = 0

See isAddUnit_iff_exists_and_exists for a similar lemma with two existentials.

source

theorem isUnit_iff_exists_and_exists {M : Type u_1} [Monoid M] {a : M} :

IsUnit a ↔ (∃ (b : M), a * b = 1) ∧ ∃ (c : M), c * a = 1

See isUnit_iff_exists for a similar lemma with one existential.

source

theorem isAddUnit_iff_exists_and_exists {M : Type u_1} [AddMonoid M] {a : M} :

IsAddUnit a ↔ (∃ (b : M), a + b = 0) ∧ ∃ (c : M), c + a = 0

See isAddUnit_iff_exists for a similar lemma with one existential.

source

@[simp]

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

IsUnit ↑u

source

@[simp]

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

IsAddUnit ↑u

source

@[simp]

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

IsUnit 1

source

@[simp]

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

IsAddUnit 0

source

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

IsUnit a

source

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

IsAddUnit a

source

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

IsUnit b

source

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

IsAddUnit b

source

theorem IsUnit.exists_right_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :

∃ (b : M), a * b = 1

source

theorem IsAddUnit.exists_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :

∃ (b : M), a + b = 0

source

theorem IsUnit.exists_left_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :

∃ (b : M), b * a = 1

source

theorem IsAddUnit.exists_neg' {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :

∃ (b : M), b + a = 0

source

theorem IsUnit.mul {M : Type u_1} [Monoid M] {a : M} {b : M} :

IsUnit a → IsUnit b → IsUnit (a * b)

source

theorem IsAddUnit.add {M : Type u_1} [AddMonoid M] {a : M} {b : M} :

IsAddUnit a → IsAddUnit b → IsAddUnit (a + b)

source

theorem IsUnit.pow {M : Type u_1} [Monoid M] {a : M} (n : ℕ) :

IsUnit a → IsUnit (a ^ n)

source

theorem IsAddUnit.nsmul {M : Type u_1} [AddMonoid M] {a : M} (n : ℕ) :

IsAddUnit a → IsAddUnit (n • a)

source

theorem isUnit_iff_eq_one {M : Type u_1} [Monoid M] [Subsingleton Mˣ] {x : M} :

IsUnit x ↔ x = 1

source

theorem isAddUnit_iff_eq_zero {M : Type u_1} [AddMonoid M] [Subsingleton (AddUnits M)] {x : M} :

IsAddUnit x ↔ x = 0

source

theorem isUnit_iff_exists_inv {M : Type u_1} [CommMonoid M] {a : M} :

IsUnit a ↔ ∃ (b : M), a * b = 1

source

theorem isAddUnit_iff_exists_neg {M : Type u_1} [AddCommMonoid M] {a : M} :

IsAddUnit a ↔ ∃ (b : M), a + b = 0

source

theorem isUnit_iff_exists_inv' {M : Type u_1} [CommMonoid M] {a : M} :

IsUnit a ↔ ∃ (b : M), b * a = 1

source

theorem isAddUnit_iff_exists_neg' {M : Type u_1} [AddCommMonoid M] {a : M} :

IsAddUnit a ↔ ∃ (b : M), b + a = 0

source

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

source

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

source

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

source

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

source

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

IsUnit x

source

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

IsAddUnit x

source

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

IsUnit y

source

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

IsAddUnit y

source

@[simp]

theorem IsUnit.mul_iff {M : Type u_1} [CommMonoid M] {x : M} {y : M} :

IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y

source

@[simp]

theorem IsAddUnit.add_iff {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} :

IsAddUnit (x + y) ↔ IsAddUnit x ∧ IsAddUnit y

source

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

h.unit = (Classical.choose h).copy a ⋯ ↑(Classical.choose h)⁻¹ ⋯

source

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

h.addUnit = (Classical.choose h).copy a ⋯ ↑(-Classical.choose h) ⋯

source

@[simp]

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

h.unit = a

source

@[simp]

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

h.addUnit = a

source

@[simp]

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

↑h.unit = a

source

@[simp]

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

↑h.addUnit = a

source

@[simp]

theorem IsUnit.unit_one {M : Type u_1} [Monoid M] (h : IsUnit 1) :

h.unit = 1

source

@[simp]

theorem IsAddUnit.addUnit_zero {M : Type u_1} [AddMonoid M] (h : IsAddUnit 0) :

h.addUnit = 0

source

@[simp]

theorem IsUnit.val_inv_mul {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :

↑h.unit⁻¹ * a = 1

source

@[simp]

theorem IsAddUnit.val_neg_add {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :

↑(-h.addUnit) + a = 0

source

@[simp]

theorem IsUnit.mul_val_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :

a * ↑h.unit⁻¹ = 1

source

@[simp]

theorem IsAddUnit.add_val_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :

a + ↑(-h.addUnit) = 0

source

instance IsUnit.instDecidableOfExistsUnitsEqVal {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.instDecidableOfExistsUnitsEqVal x = h

source

instance IsAddUnit.instDecidableOfExistsAddUnitsEqVal {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.instDecidableOfExistsAddUnitsEqVal x = h

source

@[simp]

theorem IsUnit.inv_mul_cancel {α : Type u} [DivisionMonoid α] {a : α} :

IsUnit a → a⁻¹ * a = 1

source

@[simp]

theorem IsAddUnit.neg_add_cancel {α : Type u} [SubtractionMonoid α] {a : α} :

IsAddUnit a → -a + a = 0

source

@[simp]

theorem IsUnit.mul_inv_cancel {α : Type u} [DivisionMonoid α] {a : α} :

IsUnit a → a * a⁻¹ = 1

source

@[simp]

theorem IsAddUnit.add_neg_cancel {α : Type u} [SubtractionMonoid α] {a : α} :

IsAddUnit a → a + -a = 0

source

def IsUnit.unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :

αˣ

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

Equations

h.unit' = { val := a, inv := a⁻¹, val_inv := ⋯, inv_val := ⋯ }

source

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

AddUnits α

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

Equations

h.addUnit' = { val := a, neg := -a, val_neg := ⋯, neg_val := ⋯ }

source

@[simp]

theorem IsUnit.val_unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :

↑h.unit' = a

source

@[simp]

theorem IsAddUnit.val_addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :

↑h.addUnit' = a

source

theorem IsUnit.val_inv_unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :

↑h.unit'⁻¹ = a⁻¹

source

theorem IsAddUnit.val_neg_addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :

↑(-h.addUnit') = -a

source

@[simp]

theorem IsUnit.mul_inv_cancel_left {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :

a * (a⁻¹ * b) = b

source

@[simp]

theorem IsAddUnit.add_neg_cancel_left {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :

a + (-a + b) = b

source

@[simp]

theorem IsUnit.inv_mul_cancel_left {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :

a⁻¹ * (a * b) = b

source

@[simp]

theorem IsAddUnit.neg_add_cancel_left {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :

-a + (a + b) = b

source

theorem IsUnit.div_self {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :

a / a = 1

source

theorem IsAddUnit.sub_self {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :

a - a = 0

source

theorem IsUnit.inv {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :

IsUnit a⁻¹

source

theorem IsAddUnit.neg {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :

IsAddUnit (-a)

source

theorem IsUnit.div {α : Type u} [DivisionMonoid α] {a : α} {b : α} (ha : IsUnit a) (hb : IsUnit b) :

IsUnit (a / b)

source

theorem IsAddUnit.sub {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (ha : IsAddUnit a) (hb : IsAddUnit b) :

IsAddUnit (a - b)

source

theorem IsUnit.div_mul_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :

b / (a * b) = a⁻¹

source

theorem IsAddUnit.sub_add_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :

b - (a + b) = -a

source

theorem IsUnit.mul_div_mul_right {α : Type u} [DivisionMonoid α] {c : α} (h : IsUnit c) (a : α) (b : α) :

a * c / (b * c) = a / b

source

theorem IsAddUnit.add_sub_add_right {α : Type u} [SubtractionMonoid α] {c : α} (h : IsAddUnit c) (a : α) (b : α) :

a + c - (b + c) = a - b

source

theorem IsUnit.div_mul_cancel_left {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :

a / (a * b) = b⁻¹

source

theorem IsAddUnit.sub_add_cancel_left {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :

a - (a + b) = -b

source

theorem IsUnit.mul_div_mul_left {α : Type u} [DivisionCommMonoid α] {c : α} (h : IsUnit c) (a : α) (b : α) :

c * a / (c * b) = a / b

source

theorem IsAddUnit.add_sub_add_left {α : Type u} [SubtractionCommMonoid α] {c : α} (h : IsAddUnit c) (a : α) (b : α) :

c + a - (c + b) = a - b

source

theorem divp_eq_div {α : Type u} [DivisionMonoid α] (a : α) (u : αˣ) :

a /ₚ u = a / ↑u

source

theorem Group.isUnit {α : Type u} [Group α] (a : α) :

IsUnit a

source

theorem AddGroup.isAddUnit {α : Type u} [AddGroup α] (a : α) :

IsAddUnit a

source

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

Inv M

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

Equations

invOfIsUnit h = { inv := fun (a : M) => ↑⋯.unit⁻¹ }

source

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 ⋯

source

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 ⋯

Documentation

Mathlib.Algebra.Group.Units.Defs

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

Main declarations #

Notation #

TODO #

`IsUnit` predicate #

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

Main declarations #

Notation #

TODO #

IsUnit predicate #

`IsUnit` predicate #