mathlib3 documentation

algebra.group.units

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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: add_units and is_add_unit.

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.

source
structure units (α : Type u) [monoid α] :
Type u
  • val : α
  • inv : α
  • val_inv : self.val * self.inv = 1
  • inv_val : self.inv * self.val = 1

Units of a monoid, bundled version. Notation: αˣ.

An element of a monoid is a unit if it has a two-sided inverse. This version bundles the inverse element so that it can be computed. For a predicate see is_unit.

Instances for units
source
structure add_units (α : Type u) [add_monoid α] :
Type u
  • val : α
  • neg : α
  • val_neg : self.val + self.neg = 0
  • neg_val : self.neg + self.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.

Instances for add_units
source
theorem unique_has_zero {α : Type u_1} [unique α] [has_zero α] :
inhabited.default = 0
source
theorem unique_has_one {α : Type u_1} [unique α] [has_one α] :
inhabited.default = 1
source
@[protected, instance]
def add_units.has_coe {α : Type u} [add_monoid α] :
has_coe (add_units α) α
Equations
source
@[protected, instance]
def units.has_coe {α : Type u} [monoid α] :
has_coe αˣ α
Equations
source
@[protected, instance]
def units.has_inv {α : Type u} [monoid α] :
has_inv αˣ
Equations
source
@[protected, instance]
def add_units.has_neg {α : Type u} [add_monoid α] :
has_neg (add_units α)
Equations
source
def units.simps.coe {α : Type u} [monoid α] (u : αˣ) :
α

See Note [custom simps projection]

Equations
source
def add_units.simps.coe {α : Type u} [add_monoid α] (u : add_units α) :
α

See Note [custom simps projection]

Equations
source
def units.simps.coe_inv {α : Type u} [monoid α] (u : αˣ) :
α

See Note [custom simps projection]

Equations
source
def add_units.simps.coe_neg {α : Type u} [add_monoid α] (u : add_units α) :
α

See Note [custom simps projection]

Equations
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
@[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
@[ext]
theorem units.ext {α : Type u} [monoid α] :
function.injective coe
source
@[ext]
theorem add_units.ext {α : Type u} [add_monoid α] :
function.injective coe
source
@[norm_cast]
theorem units.eq_iff {α : Type u} [monoid α] {a b : αˣ} :
↑a = ↑b ↔ a = b
source
@[norm_cast]
theorem add_units.eq_iff {α : Type u} [add_monoid α] {a b : add_units α} :
↑a = ↑b ↔ a = b
source
theorem add_units.ext_iff {α : Type u} [add_monoid α] {a b : add_units α} :
a = b ↔ ↑a = ↑b
source
theorem units.ext_iff {α : Type u} [monoid α] {a b : αˣ} :
a = b ↔ ↑a = ↑b
source
@[protected, instance]
def add_units.decidable_eq {α : Type u} [add_monoid α] [decidable_eq α] :
decidable_eq (add_units α)
Equations
source
@[protected, instance]
def units.decidable_eq {α : Type u} [monoid α] [decidable_eq α] :
decidable_eq αˣ
Equations
source
@[simp]
theorem units.mk_coe {α : 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 add_units.mk_coe {α : Type u} [add_monoid α] (u : add_units α) (y : α) (h₁ : ↑u + y = 0) (h₂ : y + ↑u = 0) :
{val := ↑u, neg := y, val_neg := h₁, neg_val := h₂} = u
source
@[simp]
theorem units.coe_copy {α : Type u} [monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹) :
↑(u.copy val hv inv hi) = val
source
@[simp]
theorem add_units.coe_copy {α : Type u} [add_monoid α] (u : add_units α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑-u) :
↑(u.copy val hv inv hi) = val
source
@[simp]
theorem units.coe_inv_copy {α : Type u} [monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹) :
↑(u.copy val hv inv hi)⁻¹ = inv
source
@[simp]
theorem add_units.coe_neg_copy {α : Type u} [add_monoid α] (u : add_units α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑-u) :
↑-u.copy 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
source
def add_units.copy {α : Type u} [add_monoid α] (u : add_units α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑-u) :
add_units α

Copy an add_unit, adjusting definitional equalities.

Equations
source
theorem add_units.copy_eq {α : Type u} [add_monoid α] (u : add_units α) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑-u) :
u.copy val hv inv hi = u
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
@[protected, instance]
def add_units.add_zero_class {α : Type u} [add_monoid α] :
add_zero_class (add_units α)
Equations
source
@[protected, instance]
def units.mul_one_class {α : Type u} [monoid α] :
mul_one_class αˣ
Equations
source
@[protected, instance]
def units.group {α : Type u} [monoid α] :
group αˣ

Units of a monoid form a group.

Equations
source
@[protected, instance]
def add_units.add_group {α : Type u} [add_monoid α] :
add_group (add_units α)

Additive units of an additive monoid form an additive group.

Equations
source
@[protected, instance]
def add_units.add_comm_group {α : Type u_1} [add_comm_monoid α] :
add_comm_group (add_units α)
Equations
source
@[protected, instance]
def units.comm_group {α : Type u_1} [comm_monoid α] :
comm_group αˣ
Equations
source
@[protected, instance]
def units.inhabited {α : Type u} [monoid α] :
inhabited αˣ
Equations
source
@[protected, instance]
def add_units.inhabited {α : Type u} [add_monoid α] :
inhabited (add_units α)
Equations
source
@[protected, instance]
def units.has_repr {α : Type u} [monoid α] [has_repr α] :
has_repr αˣ
Equations
source
@[protected, instance]
def add_units.has_repr {α : Type u} [add_monoid α] [has_repr α] :
has_repr (add_units α)
Equations
source
@[simp, norm_cast]
theorem add_units.coe_add {α : Type u} [add_monoid α] (a b : add_units α) :
↑(a + b) = ↑a + ↑b
source
@[simp, norm_cast]
theorem units.coe_mul {α : Type u} [monoid α] (a b : αˣ) :
↑(a * b) = ↑a * ↑b
source
@[simp, norm_cast]
theorem units.coe_one {α : Type u} [monoid α] :
↑1 = 1
source
@[simp, norm_cast]
theorem add_units.coe_zero {α : Type u} [add_monoid α] :
↑0 = 0
source
@[simp, norm_cast]
theorem units.coe_eq_one {α : Type u} [monoid α] {a : αˣ} :
↑a = 1 ↔ a = 1
source
@[simp, norm_cast]
theorem add_units.coe_eq_zero {α : Type u} [add_monoid α] {a : add_units α} :
↑a = 0 ↔ a = 0
source
@[simp]
theorem add_units.neg_mk {α : Type u} [add_monoid α] (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 units.val_eq_coe {α : Type u} [monoid α] (a : αˣ) :
a.val = ↑a
source
@[simp]
theorem add_units.val_eq_coe {α : Type u} [add_monoid α] (a : add_units α) :
a.val = ↑a
source
@[simp]
theorem units.inv_eq_coe_inv {α : Type u} [monoid α] (a : αˣ) :
a.inv = ↑a⁻¹
source
@[simp]
theorem add_units.neg_eq_coe_neg {α : Type u} [add_monoid α] (a : add_units α) :
a.neg = ↑-a
source
@[simp]
theorem units.inv_mul {α : Type u} [monoid α] (a : αˣ) :
↑a⁻¹ * ↑a = 1
source
@[simp]
theorem add_units.neg_add {α : Type u} [add_monoid α] (a : add_units α) :
↑-a + ↑a = 0
source
@[simp]
theorem units.mul_inv {α : Type u} [monoid α] (a : αˣ) :
↑a * ↑a⁻¹ = 1
source
@[simp]
theorem add_units.add_neg {α : Type u} [add_monoid α] (a : add_units α) :
↑a + ↑-a = 0
source
theorem add_units.neg_add_of_eq {α : Type u} [add_monoid α] {u : add_units α} {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 add_units.add_neg_of_eq {α : Type u} [add_monoid α] {u : add_units α} {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 add_units.add_neg_cancel_left {α : Type u} [add_monoid α] (a : add_units α) (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 units.inv_mul_cancel_left {α : Type u} [monoid α] (a : αˣ) (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 add_units.add_neg_cancel_right {α : Type u} [add_monoid α] (a : α) (b : add_units α) :
a + ↑b + ↑-b = a
source
@[simp]
theorem units.mul_inv_cancel_right {α : Type u} [monoid α] (a : α) (b : αˣ) :
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 : αˣ) :
a * ↑b⁻¹ * ↑b = a
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_right_inj {α : Type u} [monoid α] (a : αˣ) {b c : α} :
↑a * b = ↑a * c ↔ b = c
source
@[simp]
theorem units.mul_left_inj {α : Type u} [monoid α] (a : αˣ) {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 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 units.eq_mul_inv_iff_mul_eq {α : Type u} [monoid α] (c : αˣ) {a b : α} :
a = b * ↑c⁻¹ ↔ a * ↑c = b
source
theorem units.eq_inv_mul_iff_mul_eq {α : Type u} [monoid α] (b : αˣ) {a c : α} :
a = ↑b⁻¹ * c ↔ ↑b * a = c
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 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 : αˣ) {b c : α} :
↑a⁻¹ * b = c ↔ b = ↑a * c
source
theorem units.mul_inv_eq_iff_eq_mul {α : Type u} [monoid α] (b : αˣ) {a c : α} :
a * ↑b⁻¹ = c ↔ a = c * ↑b
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
@[protected]
theorem units.inv_eq_of_mul_eq_one_left {α : Type u} [monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) :
↑u⁻¹ = a
source
@[protected]
theorem add_units.neg_eq_of_add_eq_zero_left {α : Type u} [add_monoid α] {u : add_units α} {a : α} (h : a + ↑u = 0) :
↑-u = a
source
@[protected]
theorem add_units.neg_eq_of_add_eq_zero_right {α : Type u} [add_monoid α] {u : add_units α} {a : α} (h : ↑u + a = 0) :
↑-u = a
source
@[protected]
theorem units.inv_eq_of_mul_eq_one_right {α : Type u} [monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) :
↑u⁻¹ = a
source
@[protected]
theorem add_units.eq_neg_of_add_eq_zero_left {α : Type u} [add_monoid α] {u : add_units α} {a : α} (h : ↑u + a = 0) :
a = ↑-u
source
@[protected]
theorem units.eq_inv_of_mul_eq_one_left {α : Type u} [monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) :
a = ↑u⁻¹
source
@[protected]
theorem add_units.eq_neg_of_add_eq_zero_right {α : Type u} [add_monoid α] {u : add_units α} {a : α} (h : a + ↑u = 0) :
a = ↑-u
source
@[protected]
theorem units.eq_inv_of_mul_eq_one_right {α : Type u} [monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) :
a = ↑u⁻¹
source
@[simp]
theorem add_units.add_neg_eq_zero {α : Type u} [add_monoid α] {u : add_units α} {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 add_units.neg_add_eq_zero {α : Type u} [add_monoid α] {u : add_units α} {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 add_units.add_eq_zero_iff_eq_neg {α : Type u} [add_monoid α] {u : add_units α} {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 units.mul_eq_one_iff_inv_eq {α : Type u} [monoid α] {u : αˣ} {a : α} :
↑u * a = 1 ↔ ↑u⁻¹ = a
source
theorem add_units.add_eq_zero_iff_neg_eq {α : Type u} [add_monoid α] {u : add_units α} {a : α} :
↑u + a = 0 ↔ ↑-u = a
source
theorem add_units.neg_unique {α : Type u} [add_monoid α] {u₁ u₂ : add_units α} (h : ↑u₁ = ↑u₂) :
↑-u₁ = ↑-u₂
source
theorem units.inv_unique {α : Type u} [monoid α] {u₁ u₂ : αˣ} (h : ↑u₁ = ↑u₂) :
↑u₁⁻¹ = ↑u₂⁻¹
source
@[simp]
theorem units.coe_inv {M : Type u_1} [division_monoid M] (u : Mˣ) :
↑u⁻¹ = (↑u)⁻¹
source
@[simp]
theorem add_units.coe_neg {M : Type u_1} [subtraction_monoid M] (u : add_units M) :
↑-u = -↑u
source
def add_units.mk_of_add_eq_zero {α : Type u} [add_comm_monoid α] (a b : α) (hab : 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.

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

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

Equations
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 α] (a : α) (u : αˣ) :
α

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
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 coe_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} [comm_monoid α] (x y : α) (u : αˣ) :
x /ₚ u * y = x * y /ₚ u
source
theorem divp_eq_divp_iff {α : Type u} [comm_monoid α] {x y : α} {ux uy : αˣ} :
x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
source
theorem divp_mul_divp {α : Type u} [comm_monoid α] (x y : α) (ux uy : αˣ) :
x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
source
theorem eq_one_of_mul_right {α : Type u} [comm_monoid α] [subsingleton αˣ] {a b : α} (h : a * b = 1) :
a = 1
source
theorem eq_zero_of_add_right {α : Type u} [add_comm_monoid α] [subsingleton (add_units α)] {a b : α} (h : a + b = 0) :
a = 0
source
theorem eq_zero_of_add_left {α : Type u} [add_comm_monoid α] [subsingleton (add_units α)] {a b : α} (h : a + b = 0) :
b = 0
source
theorem eq_one_of_mul_left {α : Type u} [comm_monoid α] [subsingleton αˣ] {a b : α} (h : a * b = 1) :
b = 1
source
@[simp]
theorem add_eq_zero {α : Type u} [add_comm_monoid α] [subsingleton (add_units α)] {a b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem mul_eq_one {α : Type u} [comm_monoid α] [subsingleton αˣ] {a b : α} :
a * b = 1 ↔ a = 1 ∧ b = 1

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.

source
def is_unit {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 is_unit.

Equations
Instances for is_unit
source
def is_add_unit {M : Type u_1} [add_monoid M] (a : 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.

Equations
Instances for is_add_unit
source
theorem is_unit_of_subsingleton {M : Type u_1} [monoid M] [subsingleton M] (a : M) :
is_unit a
source
theorem is_add_unit_of_subsingleton {M : Type u_1} [add_monoid M] [subsingleton M] (a : M) :
is_add_unit a
source
@[protected, instance]
def is_unit.can_lift {M : Type u_1} [monoid M] :
can_lift M Mˣ coe is_unit
Equations
source
@[protected, instance]
def is_add_unit.can_lift {M : Type u_1} [add_monoid M] :
can_lift M (add_units M) coe is_add_unit
Equations
source
@[protected, instance]
def units.unique {M : Type u_1} [monoid M] [subsingleton M] :
unique Mˣ
Equations
source
@[protected, instance]
def add_units.unique {M : Type u_1} [add_monoid M] [subsingleton M] :
unique (add_units M)
Equations
source
@[protected, simp]
theorem units.is_unit {M : Type u_1} [monoid M] (u : Mˣ) :
is_unit ↑u
source
@[protected, simp]
theorem add_units.is_add_unit_add_unit {M : Type u_1} [add_monoid M] (u : add_units M) :
is_add_unit ↑u
source
@[simp]
theorem is_unit_one {M : Type u_1} [monoid M] :
is_unit 1
source
@[simp]
theorem is_add_unit_zero {M : Type u_1} [add_monoid M] :
is_add_unit 0
source
theorem is_unit_of_mul_eq_one {M : Type u_1} [comm_monoid M] (a b : M) (h : a * b = 1) :
is_unit a
source
theorem is_add_unit_of_add_eq_zero {M : Type u_1} [add_comm_monoid M] (a b : M) (h : a + b = 0) :
is_add_unit a
source
theorem is_unit.exists_right_inv {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
∃ (b : M), a * b = 1
source
theorem is_add_unit.exists_neg {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
∃ (b : M), a + b = 0
source
theorem is_unit.exists_left_inv {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
∃ (b : M), b * a = 1
source
theorem is_add_unit.exists_neg' {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
∃ (b : M), b + a = 0
source
theorem is_unit_iff_exists_inv {M : Type u_1} [comm_monoid M] {a : M} :
is_unit a ↔ ∃ (b : M), a * b = 1
source
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
source
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
source
theorem is_unit_iff_exists_inv' {M : Type u_1} [comm_monoid M] {a : M} :
is_unit a ↔ ∃ (b : M), b * a = 1
source
theorem is_add_unit.add {M : Type u_1} [add_monoid M] {x y : M} :
is_add_unit x → is_add_unit y → is_add_unit (x + y)
source
theorem is_unit.mul {M : Type u_1} [monoid M] {x y : M} :
is_unit x → is_unit y → is_unit (x * y)
source
@[simp]
theorem add_units.is_add_unit_add_add_units {M : Type u_1} [add_monoid M] (a : M) (u : add_units M) :
is_add_unit (a + ↑u) ↔ is_add_unit a

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

source
@[simp]
theorem units.is_unit_mul_units {M : Type u_1} [monoid M] (a : M) (u : Mˣ) :
is_unit (a * ↑u) ↔ is_unit a

Multiplication by a u : Mˣ on the right doesn't affect is_unit.

source
@[simp]
theorem add_units.is_add_unit_add_units_add {M : Type u_1} [add_monoid M] (u : add_units M) (a : M) :
is_add_unit (↑u + a) ↔ is_add_unit a

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

source
@[simp]
theorem units.is_unit_units_mul {M : Type u_1} [monoid M] (u : Mˣ) (a : M) :
is_unit (↑u * a) ↔ is_unit a

Multiplication by a u : Mˣ on the left doesn't affect is_unit.

source
theorem is_unit_of_mul_is_unit_left {M : Type u_1} [comm_monoid M] {x y : M} (hu : is_unit (x * y)) :
is_unit x
source
theorem is_add_unit_of_add_is_add_unit_left {M : Type u_1} [add_comm_monoid M] {x y : M} (hu : is_add_unit (x + y)) :
is_add_unit x
source
theorem is_add_unit_of_add_is_add_unit_right {M : Type u_1} [add_comm_monoid M] {x y : M} (hu : is_add_unit (x + y)) :
is_add_unit y
source
theorem is_unit_of_mul_is_unit_right {M : Type u_1} [comm_monoid M] {x y : M} (hu : is_unit (x * y)) :
is_unit y
source
@[simp]
theorem is_unit.mul_iff {M : Type u_1} [comm_monoid M] {x y : M} :
is_unit (x * y) ↔ is_unit x ∧ is_unit y
source
@[simp]
theorem is_add_unit.add_iff {M : Type u_1} [add_comm_monoid M] {x y : M} :
is_add_unit (x + y) ↔ is_add_unit x ∧ is_add_unit y
source
@[protected]
noncomputable def is_add_unit.add_unit {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
add_units M

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 subtraction_monoid, use is_add_unit.add_unit' instead.

Equations
source
@[protected]
noncomputable def is_unit.unit {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
Mˣ

The element of the group of units, corresponding to an element of a monoid which is a unit. When α is a division_monoid, use is_unit.unit' instead.

Equations
source
@[simp]
theorem is_unit.unit_of_coe_units {M : Type u_1} [monoid M] {a : Mˣ} (h : is_unit ↑a) :
h.unit = a
source
@[simp]
theorem is_add_unit.add_unit_of_coe_add_units {M : Type u_1} [add_monoid M] {a : add_units M} (h : is_add_unit ↑a) :
h.add_unit = a
source
@[simp]
theorem is_add_unit.add_unit_spec {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
↑(h.add_unit) = a
source
@[simp]
theorem is_unit.unit_spec {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
↑(h.unit) = a
source
@[simp]
theorem is_add_unit.coe_neg_add {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
↑-h.add_unit + a = 0
source
@[simp]
theorem is_unit.coe_inv_mul {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
↑(h.unit)⁻¹ * a = 1
source
@[simp]
theorem is_add_unit.add_coe_neg {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
a + ↑-h.add_unit = 0
source
@[simp]
theorem is_unit.mul_coe_inv {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
a * ↑(h.unit)⁻¹ = 1
source
@[protected, instance]
def is_unit.decidable {M : Type u_1} [monoid M] (x : M) [h : decidable (∃ (u : Mˣ), ↑u = x)] :
decidable (is_unit x)

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

Equations
source
@[protected, instance]
def is_add_unit.decidable {M : Type u_1} [add_monoid M] (x : M) [h : decidable (∃ (u : add_units M), ↑u = x)] :
decidable (is_add_unit x)

is_add_unit x is decidable if we can decide if x comes from `add_units M

Equations
source
theorem is_unit.mul_left_inj {M : Type u_1} [monoid M] {a b c : M} (h : is_unit a) :
b * a = c * a ↔ b = c
source
theorem is_add_unit.add_left_inj {M : Type u_1} [add_monoid M] {a b c : M} (h : is_add_unit a) :
b + a = c + a ↔ b = c
source
theorem is_add_unit.add_right_inj {M : Type u_1} [add_monoid M] {a b c : M} (h : is_add_unit a) :
a + b = a + c ↔ b = c
source
theorem is_unit.mul_right_inj {M : Type u_1} [monoid M] {a b c : M} (h : is_unit a) :
a * b = a * c ↔ b = c
source
@[protected]
theorem is_unit.mul_left_cancel {M : Type u_1} [monoid M] {a b c : M} (h : is_unit a) :
a * b = a * c → b = c
source
@[protected]
theorem is_add_unit.add_left_cancel {M : Type u_1} [add_monoid M] {a b c : M} (h : is_add_unit a) :
a + b = a + c → b = c
source
@[protected]
theorem is_add_unit.add_right_cancel {M : Type u_1} [add_monoid M] {a b c : M} (h : is_add_unit b) :
a + b = c + b → a = c
source
@[protected]
theorem is_unit.mul_right_cancel {M : Type u_1} [monoid M] {a b c : M} (h : is_unit b) :
a * b = c * b → a = c
source
@[protected]
theorem is_add_unit.add_right_injective {M : Type u_1} [add_monoid M] {a : M} (h : is_add_unit a) :
function.injective (has_add.add a)
source
@[protected]
theorem is_unit.mul_right_injective {M : Type u_1} [monoid M] {a : M} (h : is_unit a) :
function.injective (has_mul.mul a)
source
@[protected]
theorem is_add_unit.add_left_injective {M : Type u_1} [add_monoid M] {b : M} (h : is_add_unit b) :
function.injective (λ (_x : M), _x + b)
source
@[protected]
theorem is_unit.mul_left_injective {M : Type u_1} [monoid M] {b : M} (h : is_unit b) :
function.injective (λ (_x : M), _x * b)
source
@[protected, simp]
theorem is_unit.inv_mul_cancel {M : Type u_1} [division_monoid M] {a : M} :
is_unit a → a⁻¹ * a = 1
source
@[protected, simp]
theorem is_add_unit.neg_add_cancel {M : Type u_1} [subtraction_monoid M] {a : M} :
is_add_unit a → -a + a = 0
source
@[protected, simp]
theorem is_add_unit.add_neg_cancel {M : Type u_1} [subtraction_monoid M] {a : M} :
is_add_unit a → a + -a = 0
source
@[protected, simp]
theorem is_unit.mul_inv_cancel {M : Type u_1} [division_monoid M] {a : M} :
is_unit a → a * a⁻¹ = 1
source
noncomputable def group_of_is_unit {M : Type u_1} [hM : monoid M] (h : ∀ (a : M), is_unit a) :
group M

Constructs a group structure on a monoid consisting only of units.

Equations
source
noncomputable def comm_group_of_is_unit {M : Type u_1} [hM : comm_monoid M] (h : ∀ (a : M), is_unit a) :
comm_group M

Constructs a comm_group structure on a comm_monoid consisting only of units.

Equations