mathlib documentation

algebra.group.units

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

structure units (α : Type u) [monoid α] :
Type u

Units of a monoid, bundled version. 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 is_unit.

structure add_units (α : Type u) [add_monoid α] :
Type u

Units of an add_monoid, bundled version. An element of an add_monoid 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 is_add_unit.

@[instance]
def add_units.has_coe {α : Type u} [add_monoid α] :

@[instance]
def units.has_coe {α : Type u} [monoid α] :
has_coe (units α) α

Equations
@[simp]
theorem units.coe_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

@[simp]
theorem add_units.coe_mk {α : Type u} [add_monoid α] (a b : α) (h₁ : a + b = 0) (h₂ : b + a = 0) :
{val := a, neg := b, val_neg := h₁, neg_val := h₂} = a

@[ext]
theorem units.ext {α : Type u} [monoid α] :

theorem add_units.ext {α : Type u} [add_monoid α] :

theorem units.eq_iff {α : Type u} [monoid α] {a b : units α} :
a = b a = b

theorem add_units.eq_iff {α : Type u} [add_monoid α] {a b : add_units α} :
a = b a = b

theorem add_units.ext_iff {α : Type u} [add_monoid α] {a b : add_units α} :
a = b a = b

theorem units.ext_iff {α : Type u} [monoid α] {a b : units α} :
a = b a = b

@[instance]

@[instance]
def units.decidable_eq {α : Type u} [monoid α] [decidable_eq α] :

Equations
@[instance]
def units.group {α : Type u} [monoid α] :

Units of a monoid form a group.

Equations
@[instance]
def add_units.add_group {α : Type u} [add_monoid α] :

@[simp]
theorem add_units.coe_add {α : Type u} [add_monoid α] (a b : add_units α) :
(a + b) = a + b

@[simp]
theorem units.coe_mul {α : Type u} [monoid α] (a b : units α) :
a * b = (a) * b

@[simp]
theorem units.coe_one {α : Type u} [monoid α] :
1 = 1

@[simp]
theorem add_units.coe_zero {α : Type u} [add_monoid α] :
0 = 0

@[simp]
theorem units.coe_eq_one {α : Type u} [monoid α] {a : units α} :
a = 1 a = 1

@[simp]
theorem add_units.coe_eq_zero {α : Type u} [add_monoid α] {a : add_units α} :
a = 0 a = 0

theorem units.val_coe {α : Type u} [monoid α] (a : units α) :
a = a.val

theorem add_units.val_coe {α : Type u} [add_monoid α] (a : add_units α) :
a = a.val

theorem units.coe_inv {α : Type u} [monoid α] (a : units α) :

theorem add_units.coe_neg {α : Type u} [add_monoid α] (a : add_units α) :

@[simp]
theorem units.inv_mul {α : Type u} [monoid α] (a : units α) :
(a⁻¹) * a = 1

@[simp]
theorem add_units.neg_add {α : Type u} [add_monoid α] (a : add_units α) :
-a + a = 0

@[simp]
theorem units.mul_inv {α : Type u} [monoid α] (a : units α) :
(a) * a⁻¹ = 1

@[simp]
theorem add_units.add_neg {α : Type u} [add_monoid α] (a : add_units α) :
a + -a = 0

theorem add_units.neg_add_of_eq {α : Type u} [add_monoid α] {u : add_units α} {a : α} :
u = a-u + a = 0

theorem units.inv_mul_of_eq {α : Type u} [monoid α] {u : units α} {a : α} :
u = a(u⁻¹) * a = 1

theorem add_units.add_neg_of_eq {α : Type u} [add_monoid α] {u : add_units α} {a : α} :
u = aa + -u = 0

theorem units.mul_inv_of_eq {α : Type u} [monoid α] {u : units α} {a : α} :
u = aa * u⁻¹ = 1

@[simp]
theorem add_units.add_neg_cancel_left {α : Type u} [add_monoid α] (a : add_units α) (b : α) :
a + (-a + b) = b

@[simp]
theorem units.mul_inv_cancel_left {α : Type u} [monoid α] (a : units α) (b : α) :
(a) * (a⁻¹) * b = b

@[simp]
theorem units.inv_mul_cancel_left {α : Type u} [monoid α] (a : units α) (b : α) :
(a⁻¹) * (a) * b = b

@[simp]
theorem add_units.neg_add_cancel_left {α : Type u} [add_monoid α] (a : add_units α) (b : α) :
-a + (a + b) = b

@[simp]
theorem add_units.add_neg_cancel_right {α : Type u} [add_monoid α] (a : α) (b : add_units α) :
a + b + -b = a

@[simp]
theorem units.mul_inv_cancel_right {α : Type u} [monoid α] (a : α) (b : units α) :
(a * b) * b⁻¹ = a

@[simp]
theorem add_units.neg_add_cancel_right {α : Type u} [add_monoid α] (a : α) (b : add_units α) :
a + -b + b = a

@[simp]
theorem units.inv_mul_cancel_right {α : Type u} [monoid α] (a : α) (b : units α) :
(a * b⁻¹) * b = a

@[instance]
def units.inhabited {α : Type u} [monoid α] :

Equations
@[instance]
def add_units.inhabited {α : Type u} [add_monoid α] :

@[instance]

@[instance]
def units.comm_group {α : Type u_1} [comm_monoid α] :

Equations
@[instance]
def units.has_repr {α : Type u} [monoid α] [has_repr α] :

Equations
@[instance]
def add_units.has_repr {α : Type u} [add_monoid α] [has_repr α] :

@[simp]
theorem add_units.add_right_inj {α : Type u} [add_monoid α] (a : add_units α) {b c : α} :
a + b = a + c b = c

@[simp]
theorem units.mul_right_inj {α : Type u} [monoid α] (a : units α) {b c : α} :
(a) * b = (a) * c b = c

@[simp]
theorem units.mul_left_inj {α : Type u} [monoid α] (a : units α) {b c : α} :
b * a = c * a b = c

@[simp]
theorem add_units.add_left_inj {α : Type u} [add_monoid α] (a : add_units α) {b c : α} :
b + a = c + a b = c

theorem add_units.eq_add_neg_iff_add_eq {α : Type u} [add_monoid α] {c : add_units α} {a b : α} :
a = b + -c a + c = b

theorem units.eq_mul_inv_iff_mul_eq {α : Type u} [monoid α] {c : units α} {a b : α} :
a = b * c⁻¹ a * c = b

theorem units.eq_inv_mul_iff_mul_eq {α : Type u} [monoid α] (b : units α) {a c : α} :
a = (b⁻¹) * c (b) * a = c

theorem add_units.eq_neg_add_iff_add_eq {α : Type u} [add_monoid α] (b : add_units α) {a c : α} :
a = -b + c b + a = c

theorem add_units.neg_add_eq_iff_eq_add {α : Type u} [add_monoid α] (a : add_units α) {b c : α} :
-a + b = c b = a + c

theorem units.inv_mul_eq_iff_eq_mul {α : Type u} [monoid α] (a : units α) {b c : α} :
(a⁻¹) * b = c b = (a) * c

theorem units.mul_inv_eq_iff_eq_mul {α : Type u} [monoid α] (b : units α) {a c : α} :
a * b⁻¹ = c a = c * b

theorem add_units.add_neg_eq_iff_eq_add {α : Type u} [add_monoid α] (b : add_units α) {a c : α} :
a + -b = c a = c + b

theorem units.inv_eq_of_mul_eq_one {α : Type u} [monoid α] {u : units α} {a : α} :
(u) * a = 1u⁻¹ = a

theorem units.inv_unique {α : Type u} [monoid α] {u₁ u₂ : units α} :
u₁ = u₂u₁⁻¹ = u₂⁻¹

def add_units.mk_of_add_eq_zero {α : Type u} [add_comm_monoid α] (a b : α) :
a + b = 0add_units α

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

def units.mk_of_mul_eq_one {α : Type u} [comm_monoid α] (a b : α) :
a * b = 1units α

For a, b in a comm_monoid such that a * b = 1, makes a unit out of a.

Equations
@[simp]
theorem units.coe_mk_of_mul_eq_one {α : Type u} [comm_monoid α] {a b : α} (h : a * b = 1) :

@[simp]
theorem add_units.coe_mk_of_add_eq_zero {α : Type u} [add_comm_monoid α] {a b : α} (h : a + b = 0) :

def divp {α : Type u} [monoid α] :
α → units α → α

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

Equations
@[simp]
theorem divp_self {α : Type u} [monoid α] (u : units α) :
u /ₚ u = 1

@[simp]
theorem divp_one {α : Type u} [monoid α] (a : α) :
a /ₚ 1 = a

theorem divp_assoc {α : Type u} [monoid α] (a b : α) (u : units α) :
a * b /ₚ u = a * (b /ₚ u)

@[simp]
theorem divp_inv {α : Type u} [monoid α] {a : α} (u : units α) :
a /ₚ u⁻¹ = a * u

@[simp]
theorem divp_mul_cancel {α : Type u} [monoid α] (a : α) (u : units α) :
(a /ₚ u) * u = a

@[simp]
theorem mul_divp_cancel {α : Type u} [monoid α] (a : α) (u : units α) :
a * u /ₚ u = a

@[simp]
theorem divp_left_inj {α : Type u} [monoid α] (u : units α) {a b : α} :
a /ₚ u = b /ₚ u a = b

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

theorem divp_eq_iff_mul_eq {α : Type u} [monoid α] {x : α} {u : units α} {y : α} :
x /ₚ u = y y * u = x

theorem divp_eq_one_iff_eq {α : Type u} [monoid α] {a : α} {u : units α} :
a /ₚ u = 1 a = u

@[simp]
theorem one_divp {α : Type u} [monoid α] (u : units α) :

theorem divp_eq_divp_iff {α : Type u} [comm_monoid α] {x y : α} {ux uy : units α} :
x /ₚ ux = y /ₚ uy x * uy = y * ux

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

is_unit predicate

In this file we define the is_unit predicate on a monoid, and prove a few basic properties. For the bundled version see units. See also prime, associated, and irreducible in algebra/associated.

def is_unit {M : Type u_1} [monoid M] :
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 : units M, where units M is a bundled version of is_unit.

Equations
def is_add_unit {M : Type u_1} [add_monoid M] :
M → Prop

An element a : M of an add_monoid is an add_unit if it has a two-sided additive inverse. The actual definition says that a is equal to some u : add_units M, where add_units M is a bundled version of is_add_unit.

theorem is_unit_of_subsingleton {M : Type u_1} [monoid M] [subsingleton M] (a : M) :

@[simp]
theorem is_unit_unit {M : Type u_1} [monoid M] (u : units M) :

@[simp]
theorem is_add_unit_add_unit {M : Type u_1} [add_monoid M] (u : add_units M) :

@[simp]
theorem is_unit_one {M : Type u_1} [monoid M] :

@[simp]
theorem is_add_unit_zero {M : Type u_1} [add_monoid M] :

theorem is_unit_of_mul_eq_one {M : Type u_1} [comm_monoid M] (a b : M) :
a * b = 1is_unit a

theorem is_add_unit_of_add_eq_zero {M : Type u_1} [add_comm_monoid M] (a b : M) :
a + b = 0is_add_unit a

theorem is_unit_iff_exists_inv {M : Type u_1} [comm_monoid M] {a : M} :
is_unit a ∃ (b : M), a * b = 1

theorem is_add_unit_iff_exists_neg {M : Type u_1} [add_comm_monoid M] {a : M} :
is_add_unit a ∃ (b : M), a + b = 0

theorem is_add_unit_iff_exists_neg' {M : Type u_1} [add_comm_monoid M] {a : M} :
is_add_unit a ∃ (b : M), b + a = 0

theorem is_unit_iff_exists_inv' {M : Type u_1} [comm_monoid M] {a : M} :
is_unit a ∃ (b : M), b * a = 1

@[simp]
theorem add_units.is_add_unit_add_add_units {M : Type u_1} [add_monoid M] (a : M) (u : add_units M) :

Addition of a u : add_units M doesn't affect is_add_unit.

@[simp]
theorem units.is_unit_mul_units {M : Type u_1} [monoid M] (a : M) (u : units M) :

Multiplication by a u : units M doesn't affect is_unit.

theorem is_unit.mul {M : Type u_1} [monoid M] {x y : M} :
is_unit xis_unit yis_unit (x * y)

theorem is_unit_of_mul_is_unit_left {M : Type u_1} [comm_monoid M] {x y : M} :
is_unit (x * y)is_unit x

theorem is_add_unit_of_add_is_add_unit_left {M : Type u_1} [add_comm_monoid M] {x y : M} :

theorem is_unit_of_add_is_unit_right {M : Type u_1} [add_comm_monoid M] {x y : M} :

theorem is_unit_of_mul_is_unit_right {M : Type u_1} [comm_monoid M] {x y : M} :
is_unit (x * y)is_unit y

theorem is_add_unit.add_right_inj {M : Type u_1} [add_monoid M] {a b c : M} :
is_add_unit a(a + b = a + c b = c)

theorem is_unit.mul_right_inj {M : Type u_1} [monoid M] {a b c : M} :
is_unit a(a * b = a * c b = c)

theorem is_unit.mul_left_inj {M : Type u_1} [monoid M] {a b c : M} :
is_unit a(b * a = c * a b = c)

theorem is_add_unit.add_left_inj {M : Type u_1} [add_monoid M] {a b c : M} :
is_add_unit a(b + a = c + a b = c)

def is_unit.unit {M : Type u_1} [monoid M] {a : M} :
is_unit aunits M

The element of the group of units, corresponding to an element of a monoid which is a unit.

Equations
theorem is_unit.unit_spec {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
(h.unit) = a