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

An element of a Monoid is a unit if it has a two-sided inverse. This file contains the basic lemmas on units in a monoid, especially focusing on singleton types and unique types.

TODO

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

theorem unique_one {α : Type u_1} [Unique α] [One α] : default = 1

theorem unique_zero {α : Type u_1} [Unique α] [Zero α] : default = 0

@[simp]

theorem Units.mul_inv_cancel_right {α : Type u} [Monoid α] (a : α) (b : αˣ) : a * ↑b * ↑b⁻¹ = a

@[simp]

theorem AddUnits.add_neg_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) : a + ↑b + ↑(-b) = a

@[simp]

theorem Units.inv_mul_cancel_right {α : Type u} [Monoid α] (a : α) (b : αˣ) : a * ↑b⁻¹ * ↑b = a

@[simp]

theorem AddUnits.neg_add_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) : a + ↑(-b) + ↑b = a

@[simp]

theorem Units.mul_right_inj {α : Type u} [Monoid α] (a : αˣ) {b c : α} : ↑a * b = ↑a * c ↔ b = c

@[simp]

theorem AddUnits.add_right_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b c : α} : ↑a + b = ↑a + c ↔ b = c

@[simp]

theorem Units.mul_left_inj {α : Type u} [Monoid α] (a : αˣ) {b c : α} : b * ↑a = c * ↑a ↔ b = c

@[simp]

theorem AddUnits.add_left_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b c : α} : b + ↑a = c + ↑a ↔ b = c

theorem Units.eq_mul_inv_iff_mul_eq {α : Type u} [Monoid α] (c : αˣ) {a b : α} : a = b * ↑c⁻¹ ↔ a * ↑c = b

theorem AddUnits.eq_add_neg_iff_add_eq {α : Type u} [AddMonoid α] (c : AddUnits α) {a b : α} : a = b + ↑(-c) ↔ a + ↑c = b

theorem Units.eq_inv_mul_iff_mul_eq {α : Type u} [Monoid α] (b : αˣ) {a c : α} : a = ↑b⁻¹ * c ↔ ↑b * a = c

theorem AddUnits.eq_neg_add_iff_add_eq {α : Type u} [AddMonoid α] (b : AddUnits α) {a c : α} : a = ↑(-b) + c ↔ ↑b + a = c

theorem Units.mul_inv_eq_iff_eq_mul {α : Type u} [Monoid α] (b : αˣ) {a c : α} : a * ↑b⁻¹ = c ↔ a = c * ↑b

theorem AddUnits.add_neg_eq_iff_eq_add {α : Type u} [AddMonoid α] (b : AddUnits α) {a c : α} : a + ↑(-b) = c ↔ a = c + ↑b

theorem Units.inv_eq_of_mul_eq_one_left {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) : ↑u⁻¹ = a

theorem AddUnits.neg_eq_of_add_eq_zero_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 0) : ↑(-u) = a

theorem Units.inv_eq_of_mul_eq_one_right {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a

theorem AddUnits.neg_eq_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) : ↑(-u) = a

theorem Units.eq_inv_of_mul_eq_one_left {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : ↑u * a = 1) : a = ↑u⁻¹

theorem AddUnits.eq_neg_of_add_eq_zero_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) : a = ↑(-u)

theorem Units.eq_inv_of_mul_eq_one_right {α : Type u} [Monoid α] {u : αˣ} {a : α} (h : a * ↑u = 1) : a = ↑u⁻¹

theorem AddUnits.eq_neg_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 0) : a = ↑(-u)

@[simp]

theorem Units.mul_inv_eq_one {α : Type u} [Monoid α] {u : αˣ} {a : α} : a * ↑u⁻¹ = 1 ↔ a = ↑u

@[simp]

theorem AddUnits.add_neg_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : a + ↑(-u) = 0 ↔ a = ↑u

@[simp]

theorem Units.inv_mul_eq_one {α : Type u} [Monoid α] {u : αˣ} {a : α} : ↑u⁻¹ * a = 1 ↔ ↑u = a

@[simp]

theorem AddUnits.neg_add_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : ↑(-u) + a = 0 ↔ ↑u = a

theorem Units.mul_eq_one_iff_eq_inv {α : Type u} [Monoid α] {u : αˣ} {a : α} : a * ↑u = 1 ↔ a = ↑u⁻¹

theorem AddUnits.add_eq_zero_iff_eq_neg {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : a + ↑u = 0 ↔ a = ↑(-u)

theorem Units.mul_eq_one_iff_inv_eq {α : Type u} [Monoid α] {u : αˣ} {a : α} : ↑u * a = 1 ↔ ↑u⁻¹ = a

theorem AddUnits.add_eq_zero_iff_neg_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} : ↑u + a = 0 ↔ ↑(-u) = a

theorem Units.inv_unique {α : Type u} [Monoid α] {u₁ u₂ : αˣ} (h : ↑u₁ = ↑u₂) : ↑u₁⁻¹ = ↑u₂⁻¹

theorem AddUnits.neg_unique {α : Type u} [AddMonoid α] {u₁ u₂ : AddUnits α} (h : ↑u₁ = ↑u₂) : ↑(-u₁) = ↑(-u₂)

@[simp]

theorem Units.val_inv_inj {α : Type u} [Monoid α] {u₁ u₂ : αˣ} : ↑u₁⁻¹ = ↑u₂⁻¹ ↔ ↑u₁ = ↑u₂

@[simp]

theorem AddUnits.val_neg_inj {α : Type u} [AddMonoid α] {u₁ u₂ : AddUnits α} : ↑(-u₁) = ↑(-u₂) ↔ ↑u₁ = ↑u₂

theorem Units.mul_inv_eq_mul_inv_iff {α : Type u} [CommMonoid α] (a c : α) (b d : αˣ) : a * ↑b⁻¹ = c * ↑d⁻¹ ↔ a * ↑d = c * ↑b

theorem AddUnits.add_neg_eq_add_neg_iff {α : Type u} [AddCommMonoid α] (a c : α) (b d : AddUnits α) : a + ↑(-b) = c + ↑(-d) ↔ a + ↑d = c + ↑b

theorem Units.inv_mul_eq_inv_mul_iff {α : Type u} [CommMonoid α] (a c : α) (b d : αˣ) : ↑b⁻¹ * a = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b

theorem AddUnits.neg_add_eq_neg_add_iff {α : Type u} [AddCommMonoid α] (a c : α) (b d : AddUnits α) : ↑(-b) + a = ↑(-d) + c ↔ a + ↑d = c + ↑b

@[simp]

theorem divp_left_inj {α : Type u} [Monoid α] (u : αˣ) {a b : α} : a /ₚ u = b /ₚ u ↔ a = b

theorem divp_eq_iff_mul_eq {α : Type u} [Monoid α] {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * ↑u = x

theorem eq_divp_iff_mul_eq {α : Type u} [Monoid α] {x : α} {u : αˣ} {y : α} : x = y /ₚ u ↔ x * ↑u = y

theorem divp_eq_one_iff_eq {α : Type u} [Monoid α] {a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = ↑u

theorem inv_eq_one_divp' {α : Type u} [Monoid α] (u : αˣ) : ↑(1 / u) = 1 /ₚ u

theorem eq_one_of_mul_right {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} (h : a * b = 1) : a = 1

theorem eq_zero_of_add_right {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) : a = 0

theorem eq_one_of_mul_left {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} (h : a * b = 1) : b = 1

theorem eq_zero_of_add_left {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) : b = 0

@[simp]

theorem mul_eq_one {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} : a * b = 1 ↔ a = 1 ∧ b = 1

@[simp]

theorem add_eq_zero {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} : a + b = 0 ↔ a = 0 ∧ b = 0

theorem mul_ne_one {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} : a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

theorem add_ne_zero {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} : a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0

@[deprecated eq_one_of_mul_left (since := "2026-07-07")]

theorem eq_one_of_mul_left' {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} (h : a * b = 1) : b = 1

Alias of eq_one_of_mul_left.

@[deprecated eq_zero_of_add_left (since := "2026-07-07")]

theorem eq_zero_of_add_left' {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) : b = 0

Alias of eq_zero_of_add_left.

@[deprecated eq_one_of_mul_right (since := "2026-07-07")]

theorem eq_one_of_mul_right' {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} (h : a * b = 1) : a = 1

Alias of eq_one_of_mul_right.

@[deprecated eq_zero_of_add_right (since := "2026-07-07")]

theorem eq_zero_of_add_right' {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) : a = 0

Alias of eq_zero_of_add_right.

@[deprecated mul_eq_one (since := "2026-07-07")]

theorem mul_eq_one' {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} : a * b = 1 ↔ a = 1 ∧ b = 1

Alias of mul_eq_one.

@[deprecated add_eq_zero (since := "2026-07-07")]

theorem add_eq_zero' {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} : a + b = 0 ↔ a = 0 ∧ b = 0

Alias of add_eq_zero.

@[deprecated mul_ne_one (since := "2026-07-07")]

theorem mul_ne_one' {α : Type u} [Monoid α] [IsDedekindFiniteMonoid α] [Subsingleton αˣ] {a b : α} : a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Alias of mul_ne_one.

@[deprecated add_ne_zero (since := "2026-07-07")]

theorem add_ne_zero' {α : Type u} [AddMonoid α] [IsDedekindFiniteAddMonoid α] [Subsingleton (AddUnits α)] {a b : α} : a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0

Alias of add_ne_zero.

theorem divp_mul_eq_mul_divp {α : Type u} [CommMonoid α] (x y : α) (u : αˣ) : x /ₚ u * y = x * y /ₚ u

theorem divp_eq_divp_iff {α : Type u} [CommMonoid α] {x y : α} {ux uy : αˣ} : x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux

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

IsUnit predicate

theorem isUnit_of_subsingleton {M : Type u_1} [Monoid M] [Subsingleton M] (a : M) : IsUnit a

theorem isAddUnit_of_subsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] (a : M) : IsAddUnit a

instance instCanLiftUnitsValIsUnit {M : Type u_1} [Monoid M] : CanLift M Mˣ Units.val IsUnit

instance instCanLiftAddUnitsValIsAddUnit {M : Type u_1} [AddMonoid M] : CanLift M (AddUnits M) AddUnits.val IsAddUnit

@[instance_reducible]

instance instUniqueUnitsOfSubsingleton {M : Type u_1} [Monoid M] [Subsingleton M] : Unique Mˣ

A subsingleton Monoid has a unique unit.

Equations

• instUniqueUnitsOfSubsingleton = { toInhabited := Units.instInhabited, uniq := ⋯ }

@[instance_reducible]

instance instUniqueAddUnitsOfSubsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] : Unique (AddUnits M)

A subsingleton AddMonoid has a unique additive unit.

Equations

• instUniqueAddUnitsOfSubsingleton = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }

theorem IsUnit.mul_left_inj {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit a) : b * a = c * a ↔ b = c

theorem IsAddUnit.add_left_inj {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit a) : b + a = c + a ↔ b = c

theorem IsUnit.mul_right_inj {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit a) : a * b = a * c ↔ b = c

theorem IsAddUnit.add_right_inj {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit a) : a + b = a + c ↔ b = c

theorem IsUnit.mul_left_cancel {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit a) : a * b = a * c → b = c

theorem IsAddUnit.add_left_cancel {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit a) : a + b = a + c → b = c

theorem IsUnit.mul_right_cancel {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit b) : a * b = c * b → a = c

theorem IsAddUnit.add_right_cancel {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit b) : a + b = c + b → a = c

theorem IsUnit.mul_eq_right {M : Type u_1} [Monoid M] {a b : M} (h : IsUnit b) : a * b = b ↔ a = 1

theorem IsAddUnit.add_eq_right {M : Type u_1} [AddMonoid M] {a b : M} (h : IsAddUnit b) : a + b = b ↔ a = 0

theorem IsUnit.mul_eq_left {M : Type u_1} [Monoid M] {a b : M} (h : IsUnit a) : a * b = a ↔ b = 1

theorem IsAddUnit.add_eq_left {M : Type u_1} [AddMonoid M] {a b : M} (h : IsAddUnit a) : a + b = a ↔ b = 0

theorem IsUnit.mul_right_injective {M : Type u_1} [Monoid M] {a : M} (h : IsUnit a) : Function.Injective fun (x : M) => a * x

theorem IsAddUnit.add_right_injective {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) : Function.Injective fun (x : M) => a + x

theorem IsUnit.mul_left_injective {M : Type u_1} [Monoid M] {b : M} (h : IsUnit b) : Function.Injective fun (x : M) => x * b

theorem IsAddUnit.add_left_injective {M : Type u_1} [AddMonoid M] {b : M} (h : IsAddUnit b) : Function.Injective fun (x : M) => x + b

theorem IsUnit.isUnit_iff_mulLeft_bijective {M : Type u_1} [Monoid M] {a : M} : IsUnit a ↔ Function.Bijective fun (x : M) => a * x

theorem IsAddUnit.isAddUnit_iff_addLeft_bijective {M : Type u_1} [AddMonoid M] {a : M} : IsAddUnit a ↔ Function.Bijective fun (x : M) => a + x

theorem IsUnit.isUnit_iff_mulRight_bijective {M : Type u_1} [Monoid M] {a : M} : IsUnit a ↔ Function.Bijective fun (x : M) => x * a

theorem IsAddUnit.isAddUnit_iff_addRight_bijective {M : Type u_1} [AddMonoid M] {a : M} : IsAddUnit a ↔ Function.Bijective fun (x : M) => x + a

@[simp]

theorem IsUnit.mul_inv_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) : a * b * b⁻¹ = a

@[simp]

theorem IsAddUnit.add_neg_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) : a + b + -b = a

@[simp]

theorem IsUnit.inv_mul_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) : a * b⁻¹ * b = a

@[simp]

theorem IsAddUnit.neg_add_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) : a + -b + b = a

theorem IsUnit.eq_mul_inv_iff_mul_eq {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit c) : a = b * c⁻¹ ↔ a * c = b

theorem IsAddUnit.eq_add_neg_iff_add_eq {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) : a = b + -c ↔ a + c = b

theorem IsUnit.eq_inv_mul_iff_mul_eq {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit b) : a = b⁻¹ * c ↔ b * a = c

theorem IsAddUnit.eq_neg_add_iff_add_eq {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) : a = -b + c ↔ b + a = c

theorem IsUnit.inv_mul_eq_iff_eq_mul {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit a) : a⁻¹ * b = c ↔ b = a * c

theorem IsAddUnit.neg_add_eq_iff_eq_add {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit a) : -a + b = c ↔ b = a + c

theorem IsUnit.mul_inv_eq_iff_eq_mul {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit b) : a * b⁻¹ = c ↔ a = c * b

theorem IsAddUnit.add_neg_eq_iff_eq_add {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) : a + -b = c ↔ a = c + b

theorem IsUnit.mul_inv_eq_one {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit b) : a * b⁻¹ = 1 ↔ a = b

theorem IsAddUnit.add_neg_eq_zero {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) : a + -b = 0 ↔ a = b

theorem IsUnit.inv_mul_eq_one {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit a) : a⁻¹ * b = 1 ↔ a = b

theorem IsAddUnit.neg_add_eq_zero {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit a) : -a + b = 0 ↔ a = b

theorem IsUnit.mul_eq_one_iff_eq_inv {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit b) : a * b = 1 ↔ a = b⁻¹

theorem IsAddUnit.add_eq_zero_iff_eq_neg {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) : a + b = 0 ↔ a = -b

theorem IsUnit.mul_eq_one_iff_inv_eq {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit a) : a * b = 1 ↔ a⁻¹ = b

theorem IsAddUnit.add_eq_zero_iff_neg_eq {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit a) : a + b = 0 ↔ -a = b

@[simp]

theorem IsUnit.div_mul_cancel {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) : a / b * b = a

@[simp]

theorem IsAddUnit.sub_add_cancel {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) : a - b + b = a

@[simp]

theorem IsUnit.mul_div_cancel_right {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) : a * b / b = a

@[simp]

theorem IsAddUnit.add_sub_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) : a + b - b = a

theorem IsUnit.mul_one_div_cancel {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) : a * (1 / a) = 1

theorem IsAddUnit.add_zero_sub_cancel {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) : a + (0 - a) = 0

theorem IsUnit.one_div_mul_cancel {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) : 1 / a * a = 1

theorem IsAddUnit.zero_sub_add_cancel {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) : 0 - a + a = 0

theorem IsUnit.div_left_inj {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit c) : a / c = b / c ↔ a = b

theorem IsAddUnit.sub_left_inj {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) : a - c = b - c ↔ a = b

theorem IsUnit.div_eq_iff {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit b) : a / b = c ↔ a = c * b

theorem IsAddUnit.sub_eq_iff {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) : a - b = c ↔ a = c + b

theorem IsUnit.eq_div_iff {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit c) : a = b / c ↔ a * c = b

theorem IsAddUnit.eq_sub_iff {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) : a = b - c ↔ a + c = b

theorem IsUnit.div_eq_of_eq_mul {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit b) : a = c * b → a / b = c

theorem IsAddUnit.sub_eq_of_eq_add {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) : a = c + b → a - b = c

theorem IsUnit.eq_div_of_mul_eq {α : Type u} [DivisionMonoid α] {a b c : α} (h : IsUnit c) : a * c = b → a = b / c

theorem IsAddUnit.eq_sub_of_add_eq {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) : a + c = b → a = b - c

theorem IsUnit.div_eq_one_iff_eq {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit b) : a / b = 1 ↔ a = b

theorem IsAddUnit.sub_eq_zero_iff_eq {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) : a - b = 0 ↔ a = b

theorem IsUnit.div_mul_left {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit b) : b / (a * b) = 1 / a

theorem IsAddUnit.sub_add_left {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) : b - (a + b) = 0 - a

theorem IsUnit.mul_mul_div {α : Type u} [DivisionMonoid α] {b : α} (a : α) (h : IsUnit b) : a * b * (1 / b) = a

theorem IsAddUnit.add_add_sub {α : Type u} [SubtractionMonoid α] {b : α} (a : α) (h : IsAddUnit b) : a + b + (0 - b) = a

theorem IsUnit.div_mul_right {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) : a / (a * b) = 1 / b

theorem IsAddUnit.sub_add_right {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) : a - (a + b) = 0 - b

theorem IsUnit.mul_div_cancel_left {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) : a * b / a = b

theorem IsAddUnit.add_sub_cancel_left {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) : a + b - a = b

theorem IsUnit.mul_div_cancel {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) : a * (b / a) = b

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

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

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

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

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

theorem IsUnit.mul_inv_eq_mul_inv_iff {α : Type u} [DivisionCommMonoid α] {a b c d : α} (hb : IsUnit b) (hd : IsUnit d) : a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b

theorem IsAddUnit.add_neg_eq_add_neg_iff {α : Type u} [SubtractionCommMonoid α] {a b c d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) : a + -b = c + -d ↔ a + d = c + b

theorem IsUnit.inv_mul_eq_inv_mul_iff {α : Type u} [DivisionCommMonoid α] {a b c d : α} (hb : IsUnit b) (hd : IsUnit d) : b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b

theorem IsAddUnit.neg_add_eq_neg_add_iff {α : Type u} [SubtractionCommMonoid α] {a b c d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) : -b + a = -d + c ↔ a + d = c + b

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

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

theorem IsUnit.div_div_cancel_left {α : Type u} [DivisionCommMonoid α] {a b : α} (h : IsUnit a) : a / b / a = b⁻¹

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