mathlib docs: algebra.group.units

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

Type u

val : α
inv : α
val_inv : c.val * c.inv = 1
inv_val : c.inv * c.val = 1

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.

source

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

Type u

val : α
neg : α
val_neg : c.val + c.neg = 0
neg_val : c.neg + c.val = 0

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.

source

@[instance]

def units.has_coe {α : Type u} [monoid α] :

has_coe (units α) α

Equations

units.has_coe = {coe := units.val _inst_1}

source

@[instance]

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

has_coe (add_units α) α

source

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

source

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

source

@[ext]

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

function.injective coe

source

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

function.injective coe

source

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

↑a = ↑b ↔ a = b

source

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

↑a = ↑b ↔ a = b

source

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

a = b ↔ ↑a = ↑b

source

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

a = b ↔ ↑a = ↑b

source

@[instance]

def add_units.decidable_eq {α : Type u} [add_monoid α] [decidable_eq α] :

decidable_eq (add_units α)

source

@[instance]

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

decidable_eq (units α)

Equations

units.decidable_eq = λ (a b : units α), decidable_of_iff' (↑a = ↑b) units.ext_iff

source

@[instance]

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

group (units α)

Units of a monoid form a group.

Equations

units.group = {mul := λ (u₁ u₂ : units α), {val := u₁.val * u₂.val, inv := u₂.inv * u₁.inv, val_inv := _, inv_val := _}, mul_assoc := _, one := {val := 1, inv := 1, val_inv := _, inv_val := _}, one_mul := _, mul_one := _, inv := λ (u : units α), {val := u.inv, inv := u.val, val_inv := _, inv_val := _}, mul_left_inv := _}

source

@[instance]

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

add_group (add_units α)

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

↑1 = 1

source

@[simp]

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

↑0 = 0

source

@[simp]

theorem units.coe_eq_one {α : Type u} [monoid α] {a : units α} :

↑a = 1 ↔ a = 1

source

@[simp]

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

↑a = 0 ↔ a = 0

source

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

↑a = a.val

source

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

↑a = a.val

source

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

↑a⁻¹ = a.inv

source

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

↑-a = a.neg

source

@[simp]

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

↑-a + ↑a = 0

source

@[simp]

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

↑a⁻¹ * ↑a = 1

source

@[simp]

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

↑a + ↑-a = 0

source

@[simp]

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

↑a * ↑a⁻¹ = 1

source

theorem units.inv_mul_of_eq {α : Type u} [monoid α] {u : units α} {a : α} :

↑u = a → ↑u⁻¹ * a = 1

source

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

↑u = a → ↑-u + a = 0

source

theorem units.mul_inv_of_eq {α : Type u} [monoid α] {u : units α} {a : α} :

↑u = a → a * ↑u⁻¹ = 1

source

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

↑u = a → a + ↑-u = 0

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

a * ↑b * ↑b⁻¹ = a

source

@[simp]

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

a + ↑b + ↑-b = a

source

@[simp]

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

a + ↑-b + ↑b = a

source

@[simp]

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

a * ↑b⁻¹ * ↑b = a

source

@[instance]

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

inhabited (units α)

Equations

units.inhabited = {default := 1}

source

@[instance]

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

inhabited (add_units α)

source

@[instance]

def add_units.add_comm_group {α : Type u_1} [add_comm_monoid α] :

add_comm_group (add_units α)

source

@[instance]

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

comm_group (units α)

Equations

units.comm_group = {mul := group.mul units.group, mul_assoc := _, one := group.one units.group, one_mul := _, mul_one := _, inv := group.inv units.group, mul_left_inv := _, mul_comm := _}

source

@[instance]

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

has_repr (units α)

Equations

units.has_repr = {repr := repr ∘ units.val}

source

@[instance]

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

has_repr (add_units α)

source

@[simp]

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

↑a * b = ↑a * c ↔ b = c

source

@[simp]

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

↑a + b = ↑a + c ↔ b = c

source

@[simp]

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

b * ↑a = c * ↑a ↔ b = c

source

@[simp]

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

b + ↑a = c + ↑a ↔ b = c

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem units.inv_eq_of_mul_eq_one {α : Type u} [monoid α] {u : units α} {a : α} :

↑u * a = 1 → ↑u⁻¹ = a

source

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

↑u₁ = ↑u₂ → ↑u₁⁻¹ = ↑u₂⁻¹

source

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

a + b = 0 → add_units α

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

source

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

a * b = 1 → units α

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

Equations

units.mk_of_mul_eq_one a b hab = {val := a, inv := b, val_inv := hab, inv_val := _}

source

@[simp]

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

↑(units.mk_of_mul_eq_one a b h) = a

source

@[simp]

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

↑(add_units.mk_of_add_eq_zero a b h) = a

source

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

a /ₚ u = a * ↑u⁻¹

source

@[simp]

theorem divp_self {α : Type u} [monoid α] (u : units α) :

↑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 : units α) :

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

source

@[simp]

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

a /ₚ u⁻¹ = a * ↑u

source

@[simp]

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

a /ₚ u * ↑u = a

source

@[simp]

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

a * ↑u /ₚ u = a

source

@[simp]

theorem divp_left_inj {α : Type u} [monoid α] (u : units α) {a b : α} :

a /ₚ u = b /ₚ u ↔ a = b

source

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

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

source

theorem divp_eq_iff_mul_eq {α : Type u} [monoid α] {x : α} {u : units α} {y : α} :

x /ₚ u = y ↔ y * ↑u = x

source

theorem divp_eq_one_iff_eq {α : Type u} [monoid α] {a : α} {u : units α} :

a /ₚ u = 1 ↔ a = ↑u

source

@[simp]

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

1 /ₚ u = ↑u⁻¹

source

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

x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux

source

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

x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)

source

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.

source

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