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

source
theorem unique_one {α : Type u_1} [Unique α] [One α] :
default = 1
source
theorem unique_zero {α : Type u_1} [Unique α] [Zero α] :
default = 0
source
@[simp]
theorem Units.mul_inv_cancel_right {α : Type u} [Monoid α] (a : α) (b : α ˣ) :
a * ↑b * ↑b⁻¹ = a
source
@[simp]
theorem AddUnits.add_neg_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.neg_add_cancel_right {α : Type u} [AddMonoid α] (a : α) (b : AddUnits α) :
a + ↑(-b) + ↑b = a
source
@[simp]
theorem Units.mul_right_inj {α : Type u} [Monoid α] (a : α ˣ) {b c : α} :
↑a * b = ↑a * c ↔ b = c
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_left_inj {α : Type u} [Monoid α] (a : α ˣ) {b c : α} :
b * ↑a = c * ↑a ↔ b = c
source
@[simp]
theorem AddUnits.add_left_inj {α : Type u} [AddMonoid α] (a : AddUnits α) {b c : α} :
b + ↑a = c + ↑a ↔ b = c
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_add_neg_iff_add_eq {α : Type u} [AddMonoid α] (c : AddUnits α) {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 AddUnits.eq_neg_add_iff_add_eq {α : Type u} [AddMonoid α] (b : AddUnits α) {a 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 AddUnits.add_neg_eq_iff_eq_add {α : Type u} [AddMonoid α] (b : AddUnits α) {a c : α} :
a + ↑(-b) = c ↔ a = c + ↑b
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_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : a + ↑u = 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.neg_eq_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 0) :
↑(-u) = a
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_left {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : ↑u + a = 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.eq_neg_of_add_eq_zero_right {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} (h : 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.add_neg_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
a + ↑(-u) = 0 ↔ a = ↑u
source
@[simp]
theorem Units.inv_mul_eq_one {α : Type u} [Monoid α] {u : α ˣ} {a : α} :
↑u⁻¹ * a = 1 ↔ ↑u = a
source
@[simp]
theorem AddUnits.neg_add_eq_zero {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
↑(-u) + a = 0 ↔ ↑u = a
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_eq_neg {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
a + ↑u = 0 ↔ a = ↑(-u)
source
theorem Units.mul_eq_one_iff_inv_eq {α : Type u} [Monoid α] {u : α ˣ} {a : α} :
↑u * a = 1 ↔ ↑u⁻¹ = a
source
theorem AddUnits.add_eq_zero_iff_neg_eq {α : Type u} [AddMonoid α] {u : AddUnits α} {a : α} :
↑u + a = 0 ↔ ↑(-u) = a
source
theorem Units.inv_unique {α : Type u} [Monoid α] {u₁ u₂ : α ˣ} (h : ↑u₁ = ↑u₂) :
↑u₁⁻¹ = ↑u₂⁻¹
source
theorem AddUnits.neg_unique {α : Type u} [AddMonoid α] {u₁ u₂ : AddUnits α} (h : ↑u₁ = ↑u₂) :
↑(-u₁) = ↑(-u₂)
source
theorem Units.mul_inv_eq_mul_inv_iff {α : Type u} [CommMonoid α] (a c : α) (b d : α ˣ) :
a * ↑b⁻¹ = c * ↑d⁻¹ ↔ a * ↑d = c * ↑b
source
theorem AddUnits.add_neg_eq_add_neg_iff {α : Type u} [AddCommMonoid α] (a c : α) (b d : AddUnits α) :
a + ↑(-b) = c + ↑(-d) ↔ a + ↑d = c + ↑b
source
theorem Units.inv_mul_eq_inv_mul_iff {α : Type u} [CommMonoid α] (a c : α) (b d : α ˣ) :
↑b⁻¹ * a = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b
source
theorem AddUnits.neg_add_eq_neg_add_iff {α : Type u} [AddCommMonoid α] (a c : α) (b d : AddUnits α) :
↑(-b) + a = ↑(-d) + c ↔ a + ↑d = c + ↑b
source
@[simp]
theorem divp_left_inj {α : Type u} [Monoid α] (u : α ˣ) {a b : α} :
a /ₚ u = b /ₚ u ↔ a = b
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
theorem inv_eq_one_divp' {α : Type u} [Monoid α] (u : α ˣ) :
↑(1 / u) = 1 /ₚ u
source
theorem LeftCancelMonoid.eq_one_of_mul_right {α : Type u} [LeftCancelMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
a = 1
source
theorem AddLeftCancelMonoid.eq_zero_of_add_right {α : Type u} [AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
a = 0
source
theorem LeftCancelMonoid.eq_one_of_mul_left {α : Type u} [LeftCancelMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
b = 1
source
theorem AddLeftCancelMonoid.eq_zero_of_add_left {α : Type u} [AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
b = 0
source
@[simp]
theorem LeftCancelMonoid.mul_eq_one {α : Type u} [LeftCancelMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b = 1 ↔ a = 1 ∧ b = 1
source
@[simp]
theorem AddLeftCancelMonoid.add_eq_zero {α : Type u} [AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
theorem LeftCancelMonoid.mul_ne_one {α : Type u} [LeftCancelMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
source
theorem AddLeftCancelMonoid.add_ne_zero {α : Type u} [AddLeftCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
source
theorem RightCancelMonoid.eq_one_of_mul_right {α : Type u} [RightCancelMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
a = 1
source
theorem AddRightCancelMonoid.eq_zero_of_add_right {α : Type u} [AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
a = 0
source
theorem RightCancelMonoid.eq_one_of_mul_left {α : Type u} [RightCancelMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
b = 1
source
theorem AddRightCancelMonoid.eq_zero_of_add_left {α : Type u} [AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
b = 0
source
@[simp]
theorem RightCancelMonoid.mul_eq_one {α : Type u} [RightCancelMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b = 1 ↔ a = 1 ∧ b = 1
source
@[simp]
theorem AddRightCancelMonoid.add_eq_zero {α : Type u} [AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
theorem RightCancelMonoid.mul_ne_one {α : Type u} [RightCancelMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
source
theorem AddRightCancelMonoid.add_ne_zero {α : Type u} [AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
source
theorem eq_one_of_mul_right' {α : Type u} [CancelMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
a = 1
source
theorem eq_zero_of_add_right' {α : Type u} [AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
a = 0
source
theorem eq_one_of_mul_left' {α : Type u} [CancelMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
b = 1
source
theorem eq_zero_of_add_left' {α : Type u} [AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
b = 0
source
theorem mul_eq_one' {α : Type u} [CancelMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b = 1 ↔ a = 1 ∧ b = 1
source
theorem add_eq_zero' {α : Type u} [AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
theorem mul_ne_one' {α : Type u} [CancelMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
source
theorem add_ne_zero' {α : Type u} [AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
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_one_of_mul_right {α : Type u} [CommMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
a = 1
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_left {α : Type u} [CommMonoid α] [Subsingleton α ˣ] {a b : α} (h : a * b = 1) :
b = 1
source
theorem eq_zero_of_add_left {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α} (h : a + b = 0) :
b = 0
source
@[simp]
theorem mul_eq_one {α : Type u} [CommMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b = 1 ↔ a = 1 ∧ b = 1
source
@[simp]
theorem add_eq_zero {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0
source
theorem mul_ne_one {α : Type u} [CommMonoid α] [Subsingleton α ˣ] {a b : α} :
a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
source
theorem add_ne_zero {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a b : α} :
a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0

### `IsUnit` predicate #

source
theorem isUnit_of_subsingleton {M : Type u_1} [Monoid M] [Subsingleton M] (a : M) :
IsUnit a
source
theorem isAddUnit_of_subsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] (a : M) :
IsAddUnit a
source
instance instCanLiftUnitsValIsUnit {M : Type u_1} [Monoid M] :
CanLift M M ˣ Units.val IsUnit
source
instance instCanLiftAddUnitsValIsAddUnit {M : Type u_1} [AddMonoid M] :
CanLift M (AddUnits M) AddUnits.val IsAddUnit
source
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 := ⋯ }

source
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 := ⋯ }

source
theorem units_eq_one {M : Type u_1} [Monoid M] [Subsingleton M ˣ] (u : M ˣ) :
u = 1
source
theorem IsUnit.mul_left_inj {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit a) :
b * a = c * a ↔ b = c
source
theorem IsAddUnit.add_left_inj {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit a) :
b + a = c + a ↔ b = c
source
theorem IsUnit.mul_right_inj {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit a) :
a * b = a * c ↔ b = c
source
theorem IsAddUnit.add_right_inj {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit a) :
a + b = a + c ↔ b = c
source
theorem IsUnit.mul_left_cancel {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit a) :
a * b = a * c → b = c
source
theorem IsAddUnit.add_left_cancel {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit a) :
a + b = a + c → b = c
source
theorem IsUnit.mul_right_cancel {M : Type u_1} [Monoid M] {a b c : M} (h : IsUnit b) :
a * b = c * b → a = c
source
theorem IsAddUnit.add_right_cancel {M : Type u_1} [AddMonoid M] {a b c : M} (h : IsAddUnit b) :
a + b = c + b → a = c
source
theorem IsUnit.mul_eq_right {M : Type u_1} [Monoid M] {a b : M} (h : IsUnit b) :
a * b = b ↔ a = 1
source
theorem IsAddUnit.add_eq_right {M : Type u_1} [AddMonoid M] {a b : M} (h : IsAddUnit b) :
a + b = b ↔ a = 0
source
theorem IsUnit.mul_eq_left {M : Type u_1} [Monoid M] {a b : M} (h : IsUnit a) :
a * b = a ↔ b = 1
source
theorem IsAddUnit.add_eq_left {M : Type u_1} [AddMonoid M] {a b : M} (h : IsAddUnit a) :
a + b = a ↔ b = 0
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_right_injective {M : Type u_1} [AddMonoid M] {a : M} (h : IsAddUnit a) :
Function.Injective fun (x : M) => a + x
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.add_left_injective {M : Type u_1} [AddMonoid M] {b : M} (h : IsAddUnit b) :
Function.Injective fun (x : M) => x + b
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_addLeft_bijective {M : Type u_1} [AddMonoid M] {a : M} :
IsAddUnit a ↔ Function.Bijective fun (x : M) => a + x
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
theorem IsAddUnit.isAddUnit_iff_addRight_bijective {M : Type u_1} [AddMonoid M] {a : M} :
IsAddUnit a ↔ Function.Bijective fun (x : M) => x + 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.add_neg_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
@[simp]
theorem IsAddUnit.neg_add_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + -b + b = a
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_add_neg_iff_add_eq {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) :
a = b + -c ↔ a + c = b
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.eq_neg_add_iff_add_eq {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) :
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.neg_add_eq_iff_eq_add {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit a) :
-a + b = c ↔ b = a + c
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_iff_eq_add {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) :
a + -b = c ↔ a = c + b
source
theorem IsUnit.mul_inv_eq_one {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit b) :
a * b⁻¹ = 1 ↔ a = b
source
theorem IsAddUnit.add_neg_eq_zero {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) :
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.neg_add_eq_zero {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit a) :
-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_eq_neg {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) :
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
theorem IsAddUnit.add_eq_zero_iff_neg_eq {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit a) :
a + b = 0 ↔ -a = b
source
@[simp]
theorem IsUnit.div_mul_cancel {α : Type u} [DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a / b * b = a
source
@[simp]
theorem IsAddUnit.sub_add_cancel {α : 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
@[simp]
theorem IsAddUnit.add_sub_cancel_right {α : Type u} [SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + b - b = a
source
theorem IsUnit.mul_one_div_cancel {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
a * (1 / a) = 1
source
theorem IsAddUnit.add_zero_sub_cancel {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
a + (0 - a) = 0
source
theorem IsUnit.one_div_mul_cancel {α : Type u} [DivisionMonoid α] {a : α} (h : IsUnit a) :
1 / a * a = 1
source
theorem IsAddUnit.zero_sub_add_cancel {α : Type u} [SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
0 - a + a = 0
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_left_inj {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) :
a - c = b - c ↔ a = 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.sub_eq_iff {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) :
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.eq_sub_iff {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) :
a = b - c ↔ a + c = b
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.sub_eq_of_eq_add {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit b) :
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.eq_sub_of_add_eq {α : Type u} [SubtractionMonoid α] {a b c : α} (h : IsAddUnit c) :
a + c = b → a = b - c
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_eq_zero_iff_eq {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) :
a - b = 0 ↔ a = b
source
theorem IsUnit.div_mul_left {α : Type u} [DivisionMonoid α] {a b : α} (h : IsUnit b) :
b / (a * b) = 1 / a
source
theorem IsAddUnit.sub_add_left {α : Type u} [SubtractionMonoid α] {a b : α} (h : IsAddUnit b) :
b - (a + b) = 0 - a
source
theorem IsUnit.mul_mul_div {α : Type u} [DivisionMonoid α] {b : α} (a : α) (h : IsUnit b) :
a * b * (1 / b) = a
source
theorem IsAddUnit.add_add_sub {α : Type u} [SubtractionMonoid α] {b : α} (a : α) (h : IsAddUnit b) :
a + b + (0 - b) = a
source
theorem IsUnit.div_mul_right {α : Type u} [DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a / (a * b) = 1 / b
source
theorem IsAddUnit.sub_add_right {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a - (a + b) = 0 - 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_left {α : 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_cancel {α : Type u} [SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + (b - a) = 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.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.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_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.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
source
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
source
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
source
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
source
theorem IsUnit.div_div_cancel {α : Type u} [DivisionCommMonoid α] {a b : α} (h : IsUnit a) :
a / (a / b) = 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_left {α : Type u} [DivisionCommMonoid α] {a b : α} (h : IsUnit a) :
a / b / a = b⁻¹
source
theorem IsAddUnit.sub_sub_cancel_left {α : Type u} [SubtractionCommMonoid α] {a b : α} (h : IsAddUnit a) :
a - b - a = -b