Documentation

Mathlib.Algebra.Group.Units

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

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

Main declarations #

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

Notation #

We provide Mˣ as notation for Units M, resembling the notation R× 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
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
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 unique_zero {α : Type u_1} [Unique α] [Zero α] :
default = 0
source
theorem unique_one {α : Type u_1} [Unique α] [One α] :
default = 1
source
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 }
source
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 }
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
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
def AddUnits.Simps.val_neg {α : Type u} [AddMonoid α] (u : AddUnits α) :
α

See Note [custom simps projection]

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

See Note [custom simps projection]

Equations
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 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
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
  • ⋯ = ⋯
source
theorem AddUnits.ext {α : Type u} [AddMonoid α] :
Function.Injective AddUnits.val
source
theorem Units.ext {α : Type u} [Monoid α] :
Function.Injective Units.val
source
theorem AddUnits.eq_iff {α : Type u} [AddMonoid α] {a : AddUnits α} {b : AddUnits α} :
↑a = ↑b ↔ a = b
source
theorem Units.eq_iff {α : Type u} [Monoid α] {a : αˣ} {b : αˣ} :
↑a = ↑b ↔ a = b
source
theorem AddUnits.ext_iff {α : Type u} [AddMonoid α] {a : AddUnits α} {b : AddUnits α} :
a = b ↔ ↑a = ↑b
source
theorem Units.ext_iff {α : Type u} [Monoid α] {a : αˣ} {b : αˣ} :
a = b ↔ ↑a = ↑b
source
instance AddUnits.instDecidableEqAddUnits {α : Type u} [AddMonoid α] [DecidableEq α] :
DecidableEq (AddUnits α)

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

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

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

Equations
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
@[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
theorem AddUnits.copy.proof_1 {α : Type u_1} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)) :
val + inv = 0
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
  • AddUnits.copy u val hv inv hi = { val := val, neg := inv, val_neg := ⋯, neg_val := ⋯ }
source
theorem AddUnits.copy.proof_2 {α : Type u_1} [AddMonoid α] (u : AddUnits α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑(-u)) :
inv + val = 0
source
@[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
source
@[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
source
@[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
source
@[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
source
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 := ⋯, inv_val := ⋯ }
source
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
source
theorem Units.copy_eq {α : Type u} [Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹) :
Units.copy u val hv inv hi = u
source
theorem AddUnits.instAddZeroClass.proof_4 {α : Type u_1} [AddMonoid α] (u : AddUnits α) :
0 + u = u
source
theorem AddUnits.instAddZeroClass.proof_3 {α : Type u_1} [AddMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :
u₂.neg + u₁.neg + (↑u₁ + ↑u₂) = 0
source
instance AddUnits.instAddZeroClass {α : Type u} [AddMonoid α] :
AddZeroClass (AddUnits α)

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

Equations
source
theorem AddUnits.instAddZeroClass.proof_1 {α : Type u_1} [AddMonoid α] :
0 + 0 = 0
source
theorem AddUnits.instAddZeroClass.proof_5 {α : Type u_1} [AddMonoid α] (u : AddUnits α) :
u + 0 = u
source
theorem AddUnits.instAddZeroClass.proof_2 {α : Type u_1} [AddMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :
↑u₁ + ↑u₂ + (u₂.neg + u₁.neg) = 0
source
instance Units.instMulOneClass {α : Type u} [Monoid α] :
MulOneClass αˣ

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

Equations
source
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 }
source
instance Units.instInhabitedUnits {α : Type u} [Monoid α] :
Inhabited αˣ

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

Equations
  • Units.instInhabitedUnits = { default := 1 }
source
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 }
source
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 }
source
@[simp]
theorem AddUnits.val_add {α : Type u} [AddMonoid α] (a : AddUnits α) (b : AddUnits α) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem Units.val_mul {α : Type u} [Monoid α] (a : αˣ) (b : αˣ) :
↑(a * b) = ↑a * ↑b
source
@[simp]
theorem AddUnits.val_zero {α : Type u} [AddMonoid α] :
↑0 = 0
source
@[simp]
theorem Units.val_one {α : Type u} [Monoid α] :
↑1 = 1
source
@[simp]
theorem AddUnits.val_eq_zero {α : Type u} [AddMonoid α] {a : AddUnits α} :
↑a = 0 ↔ a = 0
source
@[simp]
theorem Units.val_eq_one {α : Type u} [Monoid α] {a : αˣ} :
↑a = 1 ↔ a = 1
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_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_eq_val_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :
a.neg = ↑(-a)
source
@[simp]
theorem Units.inv_eq_val_inv {α : Type u} [Monoid α] (a : αˣ) :
a.inv = ↑a⁻¹
source
@[simp]
theorem AddUnits.neg_add {α : Type u} [AddMonoid α] (a : AddUnits α) :
↑(-a) + ↑a = 0
source
@[simp]
theorem Units.inv_mul {α : Type u} [Monoid α] (a : αˣ) :
↑a⁻¹ * ↑a = 1
source
@[simp]
theorem AddUnits.add_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :
↑a + ↑(-a) = 0
source
@[simp]
theorem Units.mul_inv {α : Type u} [Monoid α] (a : αˣ) :
↑a * ↑a⁻¹ = 1
source
theorem AddUnits.addCommute_coe_neg {α : Type u} [AddMonoid α] (a : AddUnits α) :
AddCommute ↑a ↑(-a)
source
theorem Units.commute_coe_inv {α : Type u} [Monoid α] (a : αˣ) :
Commute ↑a ↑a⁻¹
source
theorem AddUnits.addCommute_neg_coe {α : Type u} [AddMonoid α] (a : AddUnits α) :
AddCommute ↑(-a) ↑a
source
theorem Units.commute_inv_coe {α : Type u} [Monoid α] (a : αˣ) :
Commute ↑a⁻¹ ↑a
source
theorem AddUnits.neg_add_of_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u = a) :
↑(-u) + a = 0
source
theorem Units.inv_mul_of_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u = a) :
↑u⁻¹ * a = 1
source
theorem AddUnits.add_neg_of_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u = a) :
a + ↑(-u) = 0
source
theorem Units.mul_inv_of_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u = a) :
a * ↑u⁻¹ = 1
source
@[simp]
theorem AddUnits.add_neg_cancel_left {α : Type u} [AddMonoid α] (a : AddUnits α) (b : α) :
↑a + (↑(-a) + b) = b
source
@[simp]
theorem Units.mul_inv_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
@[simp]
theorem Units.inv_mul_cancel_left {α : Type u} [Monoid α] (a : αˣ) (b : α) :
↑a⁻¹ * (↑a * b) = b
source
@[simp]
theorem AddUnits.add_neg_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) :
a + ↑b + ↑(-b) = a
source
@[simp]
theorem Units.mul_inv_cancel_right {α : Type u} [Monoid α] (a : α) (b : αˣ) :
a * ↑b * ↑b⁻¹ = a
source
@[simp]
theorem AddUnits.neg_add_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) :
a + ↑(-b) + ↑b = a
source
@[simp]
theorem Units.inv_mul_cancel_right {α : Type u} [Monoid α] (a : α) (b : αˣ) :
a * ↑b⁻¹ * ↑b = a
source
@[simp]
theorem AddUnits.add_right_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b : α} {c : α} :
↑a + b = ↑a + c ↔ b = c
source
@[simp]
theorem Units.mul_right_inj {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} :
↑a * b = ↑a * c ↔ b = c
source
@[simp]
theorem AddUnits.add_left_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b : α} {c : α} :
b + ↑a = c + ↑a ↔ b = c
source
@[simp]
theorem Units.mul_left_inj {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} :
b * ↑a = c * ↑a ↔ b = c
source
theorem AddUnits.eq_add_neg_iff_add_eq {α : Type u} [AddMonoid α] (c : AddUnits α) {a : α} {b : α} :
a = b + ↑(-c) ↔ a + ↑c = b
source
theorem Units.eq_mul_inv_iff_mul_eq {α : Type u} [Monoid α] (c : αˣ) {a : α} {b : α} :
a = b * ↑c⁻¹ ↔ a * ↑c = b
source
theorem AddUnits.eq_neg_add_iff_add_eq {α : Type u} [AddMonoid α] (b : AddUnits α) {a : α} {c : α} :
a = ↑(-b) + c ↔ ↑b + a = c
source
theorem Units.eq_inv_mul_iff_mul_eq {α : Type u} [Monoid α] (b : αˣ) {a : α} {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
theorem Units.inv_mul_eq_iff_eq_mul {α : Type u} [Monoid α] (a : αˣ) {b : α} {c : α} :
↑a⁻¹ * b = c ↔ b = ↑a * c
source
theorem AddUnits.add_neg_eq_iff_eq_add {α : Type u} [AddMonoid α] (b : AddUnits α) {a : α} {c : α} :
a + ↑(-b) = c ↔ a = c + ↑b
source
theorem Units.mul_inv_eq_iff_eq_mul {α : Type u} [Monoid α] (b : αˣ) {a : α} {c : α} :
a * ↑b⁻¹ = c ↔ a = c * ↑b
source
theorem AddUnits.neg_eq_of_add_eq_zero_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 0) :
↑(-u) = a
source
theorem Units.inv_eq_of_mul_eq_one_left {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) :
↑u⁻¹ = a
source
theorem AddUnits.neg_eq_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) :
↑(-u) = a
source
theorem Units.inv_eq_of_mul_eq_one_right {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) :
↑u⁻¹ = a
source
theorem AddUnits.eq_neg_of_add_eq_zero_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) :
a = ↑(-u)
source
theorem Units.eq_inv_of_mul_eq_one_left {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) :
a = ↑u⁻¹
source
theorem AddUnits.eq_neg_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 0) :
a = ↑(-u)
source
theorem Units.eq_inv_of_mul_eq_one_right {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) :
a = ↑u⁻¹
source
theorem AddUnits.instAddMonoid.proof_4 {α : Type u_1} [AddMonoid α] (n : ℕ) (a : AddUnits α) :
n • ↑a + n • ↑(-a) = 0
source
theorem AddUnits.instAddMonoid.proof_1 {α : Type u_1} [AddMonoid α] :
∀ (x x_1 x_2 : AddUnits α), x + x_1 + x_2 = x + (x_1 + x_2)
source
theorem AddUnits.instAddMonoid.proof_3 {α : Type u_1} [AddMonoid α] (a : AddUnits α) :
a + 0 = a
source
theorem AddUnits.instAddMonoid.proof_2 {α : Type u_1} [AddMonoid α] (a : AddUnits α) :
0 + a = a
source
theorem AddUnits.instAddMonoid.proof_5 {α : Type u_1} [AddMonoid α] (n : ℕ) (a : AddUnits α) :
n • ↑(-a) + n • ↑a = 0
source
instance AddUnits.instAddMonoid {α : Type u} [AddMonoid α] :
AddMonoid (AddUnits α)
Equations
  • AddUnits.instAddMonoid = let __src := inferInstance; AddMonoid.mk ⋯ ⋯ (fun (n : ℕ) (a : AddUnits α) => { val := n • ↑a, neg := n • ↑(-a), val_neg := ⋯, neg_val := ⋯ }) ⋯ ⋯
source
theorem AddUnits.instAddMonoid.proof_6 {α : Type u_1} [AddMonoid α] (a : AddUnits α) :
(fun (n : ℕ) (a : AddUnits α) => { val := n • ↑a, neg := n • ↑(-a), val_neg := ⋯, neg_val := ⋯ }) 0 a = 0
source
theorem AddUnits.instAddMonoid.proof_7 {α : Type u_1} [AddMonoid α] (n : ℕ) (a : AddUnits α) :
(fun (n : ℕ) (a : AddUnits α) => { val := n • ↑a, neg := n • ↑(-a), val_neg := ⋯, neg_val := ⋯ }) (n + 1) a = a + (fun (n : ℕ) (a : AddUnits α) => { val := n • ↑a, neg := n • ↑(-a), val_neg := ⋯, neg_val := ⋯ }) n a
source
instance Units.instMonoid {α : Type u} [Monoid α] :
Monoid αˣ
Equations
  • Units.instMonoid = let __src := inferInstance; Monoid.mk ⋯ ⋯ (fun (n : ℕ) (a : αˣ) => { val := ↑a ^ n, inv := ↑a⁻¹ ^ n, val_inv := ⋯, inv_val := ⋯ }) ⋯ ⋯
source
theorem AddUnits.instAddGroup.proof_4 {α : Type u_1} [AddMonoid α] (a : AddUnits α) :
0 • a = 0
source
theorem AddUnits.instAddGroup.proof_2 {α : Type u_1} [AddMonoid α] (a : AddUnits α) (b : AddUnits α) :
↑b + ↑(-a) + (↑a + ↑(-b)) = 0
source
abbrev AddUnits.instAddGroup.match_1 {α : Type u_1} [AddMonoid α] (motive : ℤ → AddUnits α → Sort u_2) :
(n : ℤ) → (a : AddUnits α) → ((n : ℕ) → (a : AddUnits α) → motive (Int.ofNat n) a) → ((n : ℕ) → (a : AddUnits α) → motive (Int.negSucc n) a) → motive n a
Equations
source
theorem AddUnits.instAddGroup.proof_3 {α : Type u_1} [AddMonoid α] :
∀ (a b : AddUnits α), a - b = a - b
source
instance AddUnits.instAddGroup {α : Type u} [AddMonoid α] :
AddGroup (AddUnits α)

Additive units of an additive monoid form an additive group.

Equations
  • AddUnits.instAddGroup = let __src := inferInstance; AddGroup.mk ⋯
source
theorem AddUnits.instAddGroup.proof_1 {α : Type u_1} [AddMonoid α] (a : AddUnits α) (b : AddUnits α) :
↑a + ↑(-b) + (↑b + ↑(-a)) = 0
source
theorem AddUnits.instAddGroup.proof_6 {α : Type u_1} [AddMonoid α] (n : ℕ) (a : AddUnits α) :
-(Nat.succ n • a) = -(Nat.succ n • a)
source
theorem AddUnits.instAddGroup.proof_7 {α : Type u_1} [AddMonoid α] (u : AddUnits α) :
-u + u = 0
source
theorem AddUnits.instAddGroup.proof_5 {α : Type u_1} [AddMonoid α] (n : ℕ) (a : AddUnits α) :
(n + 1) • a = a + n • a
source
instance Units.instGroup {α : Type u} [Monoid α] :
Group αˣ

Units of a monoid form a group.

Equations
  • Units.instGroup = let __src := inferInstance; Group.mk ⋯
source
theorem AddUnits.instAddCommGroupAddUnits.proof_1 {α : Type u_1} [AddCommMonoid α] :
∀ (x x_1 : AddUnits α), x + x_1 = x_1 + x
source
instance AddUnits.instAddCommGroupAddUnits {α : Type u_1} [AddCommMonoid α] :
AddCommGroup (AddUnits α)

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

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

Units of a commutative monoid form a commutative group.

Equations
source
@[simp]
theorem AddUnits.val_nsmul_eq_nsmul_val {α : Type u} [AddMonoid α] (a : AddUnits α) (n : ℕ) :
↑(n • a) = n • ↑a
source
@[simp]
theorem Units.val_pow_eq_pow_val {α : Type u} [Monoid α] (a : αˣ) (n : ℕ) :
↑(a ^ n) = ↑a ^ n
source
@[simp]
theorem AddUnits.add_neg_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
a + ↑(-u) = 0 ↔ a = ↑u
source
@[simp]
theorem Units.mul_inv_eq_one {α : Type u} [Monoid α] {u : αˣ} {a : α} :
a * ↑u⁻¹ = 1 ↔ a = ↑u
source
@[simp]
theorem AddUnits.neg_add_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
↑(-u) + a = 0 ↔ ↑u = a
source
@[simp]
theorem Units.inv_mul_eq_one {α : Type u} [Monoid α] {u : αˣ} {a : α} :
↑u⁻¹ * a = 1 ↔ ↑u = a
source
theorem AddUnits.add_eq_zero_iff_eq_neg {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
a + ↑u = 0 ↔ a = ↑(-u)
source
theorem Units.mul_eq_one_iff_eq_inv {α : Type u} [Monoid α] {u : αˣ} {a : α} :
a * ↑u = 1 ↔ a = ↑u⁻¹
source
theorem AddUnits.add_eq_zero_iff_neg_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
↑u + a = 0 ↔ ↑(-u) = a
source
theorem Units.mul_eq_one_iff_inv_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} :
↑u * a = 1 ↔ ↑u⁻¹ = a
source
theorem AddUnits.neg_unique {α : Type u} [AddMonoid α] {u₁ : AddUnits α} {u₂ : AddUnits α} (h : ↑u₁ = ↑u₂) :
↑(-u₁) = ↑(-u₂)
source
theorem Units.inv_unique {α : Type u} [Monoid α] {u₁ : αˣ} {u₂ : αˣ} (h : ↑u₁ = ↑u₂) :
↑u₁⁻¹ = ↑u₂⁻¹
source
@[simp]
theorem AddUnits.val_neg_eq_neg_val {α : Type u} [SubtractionMonoid α] (u : AddUnits α) :
↑(-u) = -↑u
source
@[simp]
theorem Units.val_inv_eq_inv_val {α : Type u} [DivisionMonoid α] (u : αˣ) :
↑u⁻¹ = (↑u)⁻¹
source
@[simp]
theorem AddUnits.val_sub_eq_sub_val {α : Type u} [SubtractionMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :
↑(u₁ - u₂) = ↑u₁ - ↑u₂
source
@[simp]
theorem Units.val_div_eq_div_val {α : Type u} [DivisionMonoid α] (u₁ : αˣ) (u₂ : αˣ) :
↑(u₁ / u₂) = ↑u₁ / ↑u₂
source
theorem AddUnits.mkOfAddEqZero.proof_1 {α : Type u_1} [AddCommMonoid α] (a : α) (b : α) (hab : a + b = 0) :
b + a = 0
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
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
source
@[simp]
theorem AddUnits.val_mkOfAddEqZero {α : Type u} [AddCommMonoid α] {a : α} {b : α} (h : a + b = 0) :
↑(AddUnits.mkOfAddEqZero a b h) = a
source
@[simp]
theorem Units.val_mkOfMulEqOne {α : Type u} [CommMonoid α] {a : α} {b : α} (h : a * b = 1) :
↑(Units.mkOfMulEqOne 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
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
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
@[simp]
theorem divp_left_inj {α : Type u} [Monoid α] (u : αˣ) {a : α} {b : α} :
a /ₚ u = b /ₚ u ↔ a = b
source
theorem divp_divp_eq_divp_mul {α : Type u} [Monoid α] (x : α) (u₁ : αˣ) (u₂ : αˣ) :
x /ₚ u₁ /ₚ u₂ = x /ₚ (u₂ * u₁)
source
theorem divp_eq_iff_mul_eq {α : Type u} [Monoid α] {x : α} {u : αˣ} {y : α} :
x /ₚ u = y ↔ y * ↑u = x
source
theorem eq_divp_iff_mul_eq {α : Type u} [Monoid α] {x : α} {u : αˣ} {y : α} :
x = y /ₚ u ↔ x * ↑u = y
source
theorem divp_eq_one_iff_eq {α : Type u} [Monoid α] {a : α} {u : αˣ} :
a /ₚ u = 1 ↔ a = ↑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 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).

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

source
theorem divp_mul_eq_mul_divp {α : Type u} [CommMonoid α] (x : α) (y : α) (u : αˣ) :
x /ₚ u * y = x * y /ₚ u
source
theorem divp_eq_divp_iff {α : Type u} [CommMonoid α] {x : α} {y : α} {ux : αˣ} {uy : αˣ} :
x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
source
theorem divp_mul_divp {α : Type u} [CommMonoid α] (x : α) (y : α) (ux : αˣ) (uy : αˣ) :
x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
source
theorem eq_zero_of_add_right {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} (h : a + b = 0) :
a = 0
source
theorem eq_one_of_mul_right {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} (h : a * b = 1) :
a = 1
source
theorem eq_zero_of_add_left {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} (h : a + b = 0) :
b = 0
source
theorem eq_one_of_mul_left {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} (h : a * b = 1) :
b = 1
source
@[simp]
theorem add_eq_zero {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem mul_eq_one {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} :
a * b = 1 ↔ a = 1 ∧ b = 1

IsUnit predicate #

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
Instances For
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
Instances For
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
abbrev isAddUnit_iff_exists.match_2 {M : Type u_1} [AddMonoid M] {x : M} (motive : (∃ (b : M), x + b = 0 ∧ b + x = 0) → Prop) :
∀ (x_1 : ∃ (b : M), x + b = 0 ∧ b + x = 0), (∀ (b : M) (h1b : x + b = 0) (h2b : b + x = 0), motive ⋯) → motive x_1
Equations
  • ⋯ = ⋯
source
abbrev isAddUnit_iff_exists.match_1 {M : Type u_1} [AddMonoid M] {x : M} (motive : IsAddUnit x → Prop) :
∀ (x_1 : IsAddUnit x), (∀ (u : AddUnits M) (hu : ↑u = x), motive ⋯) → motive x_1
Equations
  • ⋯ = ⋯
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_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
abbrev isAddUnit_iff_exists_and_exists.match_1 {M : Type u_1} [AddMonoid M] {a : M} (motive : ((∃ (b : M), a + b = 0) ∧ ∃ (c : M), c + a = 0) → Prop) :
∀ (x : (∃ (b : M), a + b = 0) ∧ ∃ (c : M), c + a = 0), (∀ (b : M) (hb : a + b = 0) (w : M) (hc : w + a = 0), motive ⋯) → motive x
Equations
  • ⋯ = ⋯
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_of_subsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] (a : M) :
IsAddUnit a
source
theorem isUnit_of_subsingleton {M : Type u_1} [Monoid M] [Subsingleton M] (a : M) :
IsUnit a
source
instance instCanLiftAddUnitsValIsAddUnit {M : Type u_1} [AddMonoid M] :
CanLift M (AddUnits M) AddUnits.val IsAddUnit
Equations
  • ⋯ = ⋯
source
instance instCanLiftUnitsValIsUnit {M : Type u_1} [Monoid M] :
CanLift M Mˣ Units.val IsUnit
Equations
  • ⋯ = ⋯
source
theorem instUniqueAddUnits.proof_1 {M : Type u_1} [AddMonoid M] [Subsingleton M] (a : AddUnits M) :
a = 0
source
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 := ⋯ }
source
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 := ⋯ }
source
@[simp]
theorem AddUnits.isAddUnit {M : Type u_1} [AddMonoid M] (u : AddUnits M) :
IsAddUnit ↑u
source
@[simp]
theorem Units.isUnit {M : Type u_1} [Monoid M] (u : Mˣ) :
IsUnit ↑u
source
@[simp]
theorem isAddUnit_zero {M : Type u_1} [AddMonoid M] :
IsAddUnit 0
source
@[simp]
theorem isUnit_one {M : Type u_1} [Monoid M] :
IsUnit 1
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 {M : Type u_1} [CommMonoid M] (a : M) (b : M) (h : a * b = 1) :
IsUnit a
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_of_mul_eq_one_right {M : Type u_1} [CommMonoid M] (a : M) (b : M) (h : a * b = 1) :
IsUnit b
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_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), b + a = 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.add {M : Type u_1} [AddMonoid M] {a : M} {b : M} :
IsAddUnit a → IsAddUnit b → IsAddUnit (a + b)
source
theorem IsUnit.mul {M : Type u_1} [Monoid M] {a : M} {b : M} :
IsUnit a → IsUnit b → IsUnit (a * b)
source
theorem IsAddUnit.nsmul {M : Type u_1} [AddMonoid M] {a : M} (n : ℕ) :
IsAddUnit a → IsAddUnit (n • a)
source
theorem IsUnit.pow {M : Type u_1} [Monoid M] {a : M} (n : ℕ) :
IsUnit a → IsUnit (a ^ n)
source
theorem units_eq_one {M : Type u_1} [Monoid M] [Unique Mˣ] (u : Mˣ) :
u = 1
source
theorem isAddUnit_iff_eq_zero {M : Type u_1} [AddMonoid M] [Unique (AddUnits M)] {x : M} :
IsAddUnit x ↔ x = 0
source
theorem isUnit_iff_eq_one {M : Type u_1} [Monoid M] [Unique Mˣ] {x : M} :
IsUnit x ↔ x = 1
source
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 ⋯) → motive x
Equations
  • ⋯ = ⋯
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), a * b = 1
source
theorem isAddUnit_iff_exists_neg' {M : Type u_1} [AddCommMonoid M] {a : M} :
IsAddUnit a ↔ ∃ (b : M), b + a = 0
source
theorem isUnit_iff_exists_inv' {M : Type u_1} [CommMonoid M] {a : M} :
IsUnit a ↔ ∃ (b : M), b * a = 1
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
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 ⋯) → motive x
Equations
  • ⋯ = ⋯
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
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 ⋯) → motive x
Equations
  • ⋯ = ⋯
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
@[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
theorem isAddUnit_of_add_isAddUnit_left {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} (hu : IsAddUnit (x + y)) :
IsAddUnit x
source
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 ⋯) → motive x_1
Equations
  • ⋯ = ⋯
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_right {M : Type u_1} [AddCommMonoid M] {x : M} {y : M} (hu : IsAddUnit (x + y)) :
IsAddUnit y
source
theorem isUnit_of_mul_isUnit_right {M : Type u_1} [CommMonoid M] {x : M} {y : M} (hu : IsUnit (x * y)) :
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
@[simp]
theorem IsUnit.mul_iff {M : Type u_1} [CommMonoid M] {x : M} {y : M} :
IsUnit (x * y) ↔ IsUnit x ∧ IsUnit 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
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
source
@[simp]
theorem IsAddUnit.addUnit_of_val_addUnits {M : Type u_1} [AddMonoid M] {a : AddUnits M} (h : IsAddUnit ↑a) :
IsAddUnit.addUnit h = a
source
@[simp]
theorem IsUnit.unit_of_val_units {M : Type u_1} [Monoid M] {a : Mˣ} (h : IsUnit ↑a) :
IsUnit.unit h = a
source
@[simp]
theorem IsAddUnit.addUnit_spec {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
↑(IsAddUnit.addUnit h) = a
source
@[simp]
theorem IsUnit.unit_spec {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
↑(IsUnit.unit h) = a
source
@[simp]
theorem IsAddUnit.val_neg_add {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
↑(-IsAddUnit.addUnit h) + a = 0
source
@[simp]
theorem IsUnit.val_inv_mul {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
↑(IsUnit.unit h)⁻¹ * a = 1
source
@[simp]
theorem IsAddUnit.add_val_neg {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
a + ↑(-IsAddUnit.addUnit h) = 0
source
@[simp]
theorem IsUnit.mul_val_inv {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
a * ↑(IsUnit.unit h)⁻¹ = 1
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem IsAddUnit.add_right_injective {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
Function.Injective fun (x : M) => a + x
source
theorem IsUnit.mul_right_injective {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) :
Function.Injective fun (x : M) => a * x
source
theorem IsAddUnit.add_left_injective {M : Type u_1} [AddMonoid M] {b : M} (h : IsAddUnit b) :
Function.Injective fun (x : M) => x + b
source
theorem IsUnit.mul_left_injective {M : Type u_1} [Monoid M] {b : M} (h : IsUnit b) :
Function.Injective fun (x : M) => x * b
source
theorem IsAddUnit.isAddUnit_iff_addLeft_bijective {M : Type u_1} [AddMonoid M] {a : M} :
IsAddUnit a ↔ Function.Bijective fun (x : M) => a + x
source
theorem IsUnit.isUnit_iff_mulLeft_bijective {M : Type u_1} [Monoid M] {a : M} :
IsUnit a ↔ Function.Bijective fun (x : M) => a * x
source
theorem IsAddUnit.isAddUnit_iff_addRight_bijective {M : Type u_1} [AddMonoid M] {a : M} :
IsAddUnit a ↔ Function.Bijective fun (x : M) => x + a
source
theorem IsUnit.isUnit_iff_mulRight_bijective {M : Type u_1} [Monoid M] {a : M} :
IsUnit a ↔ Function.Bijective fun (x : M) => x * a
source
@[simp]
theorem IsAddUnit.neg_add_cancel {α : Type u} [SubtractionMonoid α] {a : α} :
IsAddUnit a → -a + a = 0
source
@[simp]
theorem IsUnit.inv_mul_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
@[simp]
theorem IsUnit.mul_inv_cancel {α : Type u} [DivisionMonoid α] {a : α} :
IsUnit a → a * a⁻¹ = 1
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
source
@[simp]
theorem IsAddUnit.val_addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
↑(IsAddUnit.addUnit' h) = a
source
@[simp]
theorem IsUnit.val_unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
↑(IsUnit.unit' h) = a
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
source
theorem IsAddUnit.val_neg_addUnit' {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
↑(-IsAddUnit.addUnit' h) = -a
source
theorem IsUnit.val_inv_unit' {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
↑(IsUnit.unit' h)⁻¹ = a⁻¹
source
@[simp]
theorem IsAddUnit.add_neg_cancel_left {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + (-a + b) = b
source
@[simp]
theorem IsUnit.mul_inv_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
@[simp]
theorem IsUnit.inv_mul_cancel_left {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :
a⁻¹ * (a * b) = b
source
@[simp]
theorem IsAddUnit.add_neg_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + b + -b = a
source
@[simp]
theorem IsUnit.mul_inv_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a * b * b⁻¹ = a
source
@[simp]
theorem IsAddUnit.neg_add_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + -b + b = a
source
@[simp]
theorem IsUnit.inv_mul_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a * b⁻¹ * b = a
source
theorem IsAddUnit.sub_self {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
a - a = 0
source
theorem IsUnit.div_self {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
a / a = 1
source
theorem IsAddUnit.eq_add_neg_iff_add_eq {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a = b + -c ↔ a + c = b
source
theorem IsUnit.eq_mul_inv_iff_mul_eq {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a = b * c⁻¹ ↔ a * c = b
source
theorem IsAddUnit.eq_neg_add_iff_add_eq {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a = -b + c ↔ b + a = c
source
theorem IsUnit.eq_inv_mul_iff_mul_eq {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a = b⁻¹ * c ↔ b * a = c
source
theorem IsAddUnit.neg_add_eq_iff_eq_add {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit a) :
-a + b = c ↔ b = a + c
source
theorem IsUnit.inv_mul_eq_iff_eq_mul {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit a) :
a⁻¹ * b = c ↔ b = a * c
source
theorem IsAddUnit.add_neg_eq_iff_eq_add {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a + -b = c ↔ a = c + b
source
theorem IsUnit.mul_inv_eq_iff_eq_mul {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a * b⁻¹ = c ↔ a = c * b
source
theorem IsAddUnit.add_neg_eq_zero {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
a + -b = 0 ↔ a = b
source
theorem IsUnit.mul_inv_eq_one {α : Type u} [DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
a * b⁻¹ = 1 ↔ a = b
source
theorem IsAddUnit.neg_add_eq_zero {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
-a + b = 0 ↔ a = b
source
theorem IsUnit.inv_mul_eq_one {α : Type u} [DivisionMonoid α] {a : α} {b : α} (h : IsUnit a) :
a⁻¹ * b = 1 ↔ a = b
source
theorem IsAddUnit.add_eq_zero_iff_eq_neg {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
a + b = 0 ↔ a = -b
source
theorem IsUnit.mul_eq_one_iff_eq_inv {α : Type u} [DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
a * b = 1 ↔ a = b⁻¹
source
theorem IsAddUnit.add_eq_zero_iff_neg_eq {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
a + b = 0 ↔ -a = b
source
theorem IsUnit.mul_eq_one_iff_inv_eq {α : Type u} [DivisionMonoid α] {a : α} {b : α} (h : IsUnit a) :
a * b = 1 ↔ a⁻¹ = b
source
@[simp]
theorem IsAddUnit.sub_add_cancel {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a - b + b = a
source
@[simp]
theorem IsUnit.div_mul_cancel {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a / b * b = a
source
@[simp]
theorem IsAddUnit.add_sub_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + b - b = a
source
@[simp]
theorem IsUnit.mul_div_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a * b / b = a
source
theorem IsAddUnit.add_zero_sub_cancel {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
a + (0 - a) = 0
source
theorem IsUnit.mul_one_div_cancel {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
a * (1 / a) = 1
source
theorem IsAddUnit.zero_sub_add_cancel {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
0 - a + a = 0
source
theorem IsUnit.one_div_mul_cancel {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
1 / a * a = 1
source
theorem IsAddUnit.neg {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
IsAddUnit (-a)
source
theorem IsUnit.inv {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
IsUnit a⁻¹
source
theorem IsAddUnit.sub {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (ha : IsAddUnit a) (hb : IsAddUnit b) :
IsAddUnit (a - b)
source
theorem IsUnit.div {α : Type u} [DivisionMonoid α] {a : α} {b : α} (ha : IsUnit a) (hb : IsUnit b) :
IsUnit (a / b)
source
theorem IsAddUnit.sub_left_inj {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a - c = b - c ↔ a = b
source
theorem IsUnit.div_left_inj {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a / c = b / c ↔ a = b
source
theorem IsAddUnit.sub_eq_iff {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a - b = c ↔ a = c + b
source
theorem IsUnit.div_eq_iff {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a / b = c ↔ a = c * b
source
theorem IsAddUnit.eq_sub_iff {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a = b - c ↔ a + c = b
source
theorem IsUnit.eq_div_iff {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a = b / c ↔ a * c = b
source
theorem IsAddUnit.sub_eq_of_eq_add {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a = c + b → a - b = c
source
theorem IsUnit.div_eq_of_eq_mul {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a = c * b → a / b = c
source
theorem IsAddUnit.eq_sub_of_add_eq {α : Type u} [SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a + c = b → a = b - c
source
theorem IsUnit.eq_div_of_mul_eq {α : Type u} [DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a * c = b → a = b / c
source
theorem IsAddUnit.sub_eq_zero_iff_eq {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
a - b = 0 ↔ a = b
source
theorem IsUnit.div_eq_one_iff_eq {α : Type u} [DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
a / b = 1 ↔ a = b
source
theorem IsAddUnit.sub_add_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
b - (a + b) = -a
source
theorem IsUnit.div_mul_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
b / (a * b) = a⁻¹
source
@[deprecated sub_add_cancel_right]
theorem IsAddUnit.sub_add_left {α : Type u} [SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
b - (a + b) = 0 - a
source
@[deprecated div_mul_cancel_right]
theorem IsUnit.div_mul_left {α : Type u} [DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
b / (a * b) = 1 / a
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.mul_div_mul_right {α : Type u} [DivisionMonoid α] {c : α} (h : IsUnit c) (a : α) (b : α) :
a * c / (b * c) = a / b
source
theorem IsAddUnit.add_add_sub {α : Type u} [SubtractionMonoid α] {b : α} (a : α) (h : IsAddUnit b) :
a + b + (0 - b) = a
source
theorem IsUnit.mul_mul_div {α : Type u} [DivisionMonoid α] {b : α} (a : α) (h : IsUnit b) :
a * b * (1 / b) = a
source
theorem IsAddUnit.sub_add_cancel_left {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a - (a + b) = -b
source
theorem IsUnit.div_mul_cancel_left {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a / (a * b) = b⁻¹
source
@[deprecated sub_add_cancel_left]
theorem IsAddUnit.sub_add_right {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a - (a + b) = 0 - b
source
@[deprecated div_mul_cancel_left]
theorem IsUnit.div_mul_right {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a / (a * b) = 1 / b
source
theorem IsAddUnit.add_sub_cancel_left {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + b - a = b
source
theorem IsUnit.mul_div_cancel_left {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a * b / a = b
source
theorem IsAddUnit.add_sub_cancel {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + (b - a) = b
source
theorem IsUnit.mul_div_cancel {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a * (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 IsUnit.mul_div_mul_left {α : Type u} [DivisionCommMonoid α] {c : α} (h : IsUnit c) (a : α) (b : α) :
c * a / (c * b) = a / b
source
theorem IsAddUnit.add_eq_add_of_sub_eq_sub {α : Type u} [SubtractionCommMonoid α] {b : α} {d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) (a : α) (c : α) (h : a - b = c - d) :
a + d = c + b
source
theorem IsUnit.mul_eq_mul_of_div_eq_div {α : Type u} [DivisionCommMonoid α] {b : α} {d : α} (hb : IsUnit b) (hd : IsUnit d) (a : α) (c : α) (h : a / b = c / d) :
a * d = c * b
source
theorem IsAddUnit.sub_eq_sub_iff {α : Type u} [SubtractionCommMonoid α] {a : α} {b : α} {c : α} {d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) :
a - b = c - d ↔ a + d = c + b
source
theorem IsUnit.div_eq_div_iff {α : Type u} [DivisionCommMonoid α] {a : α} {b : α} {c : α} {d : α} (hb : IsUnit b) (hd : IsUnit d) :
a / b = c / d ↔ a * d = c * b
source
theorem IsAddUnit.sub_sub_cancel {α : Type u} [SubtractionCommMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
a - (a - b) = b
source
theorem IsUnit.div_div_cancel {α : Type u} [DivisionCommMonoid α] {a : α} {b : α} (h : IsUnit a) :
a / (a / b) = b
source
theorem IsAddUnit.sub_sub_cancel_left {α : Type u} [SubtractionCommMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
a - b - a = -b
source
theorem IsUnit.div_div_cancel_left {α : Type u} [DivisionCommMonoid α] {a : α} {b : α} (h : IsUnit a) :
a / b / a = b⁻¹
source
theorem divp_eq_div {α : Type u} [DivisionMonoid α] (a : α) (u : αˣ) :
a /ₚ u = a / ↑u
source
theorem AddGroup.isAddUnit {α : Type u} [AddGroup α] (a : α) :
IsAddUnit a
source
theorem Group.isUnit {α : Type u} [Group α] (a : α) :
IsUnit a
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
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
source
@[deprecated IsUnit.mul_div_cancel]
theorem IsUnit.mul_div_cancel' {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a * (b / a) = b

Alias of IsUnit.mul_div_cancel.

source
@[deprecated IsAddUnit.add_sub_cancel]
theorem IsAddUnit.add_sub_cancel' {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + (b - a) = b

Alias of IsAddUnit.add_sub_cancel.