# Documentation

Mathlib.Algebra.Hom.Units

# Monoid homomorphisms and units #

This file allows to lift monoid homomorphisms to group homomorphisms of their units subgroups. It also contains unrelated results about Units that depend on MonoidHom.

## Main declarations #

• Units.map: Turn a homomorphism from α to β monoids into a homomorphism from αˣ to βˣ.
• MonoidHom.toHomUnits: Turn a homomorphism from a group α to β into a homomorphism from α to βˣ.

## TODO #

The results that don't mention homomorphisms should be proved (earlier?) in a different file and be used to golf the basic Group lemmas.

theorem Group.isUnit {G : Type u_1} [] (g : G) :
theorem IsAddUnit.eq_on_neg {F : Type u_1} {G : Type u_2} {N : Type u_3} [] [] {x : G} (hx : ) (f : F) (g : F) (h : f x = g x) :
f (-x) = g (-x)

If two homomorphisms from a subtraction monoid to an additive monoid are equal at an additive unit x, then they are equal at -x.

theorem IsUnit.eq_on_inv {F : Type u_1} {G : Type u_2} {N : Type u_3} [] [] [] {x : G} (hx : ) (f : F) (g : F) (h : f x = g x) :
f x⁻¹ = g x⁻¹

If two homomorphisms from a division monoid to a monoid are equal at a unit x, then they are equal at x⁻¹.

theorem eq_on_neg {F : Type u_1} {G : Type u_2} {M : Type u_3} [] [] [] (f : F) (g : F) {x : G} (h : f x = g x) :
f (-x) = g (-x)

If two homomorphism from an additive group to an additive monoid are equal at x, then they are equal at -x.

theorem eq_on_inv {F : Type u_1} {G : Type u_2} {M : Type u_3} [] [] [] (f : F) (g : F) {x : G} (h : f x = g x) :
f x⁻¹ = g x⁻¹

If two homomorphism from a group to a monoid are equal at x, then they are equal at x⁻¹.

def AddUnits.map {M : Type u} {N : Type v} [] [] (f : M →+ N) :

The additive homomorphism on AddUnits induced by an AddMonoidHom.

Instances For
theorem AddUnits.map.proof_3 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (x : ) (y : ) :
(fun u => { val := f u, neg := f u.neg, val_neg := (_ : f u + f u.neg = 0), neg_val := (_ : f u.neg + f u = 0) }) (x + y) = (fun u => { val := f u, neg := f u.neg, val_neg := (_ : f u + f u.neg = 0), neg_val := (_ : f u.neg + f u = 0) }) x + (fun u => { val := f u, neg := f u.neg, val_neg := (_ : f u + f u.neg = 0), neg_val := (_ : f u.neg + f u = 0) }) y
theorem AddUnits.map.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (u : ) :
f u + f u.neg = 0
theorem AddUnits.map.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (u : ) :
f u.neg + f u = 0
def Units.map {M : Type u} {N : Type v} [] [] (f : M →* N) :

The group homomorphism on units induced by a MonoidHom.

Instances For
@[simp]
theorem AddUnits.coe_map {M : Type u} {N : Type v} [] [] (f : M →+ N) (x : ) :
↑(↑() x) = f x
@[simp]
theorem Units.coe_map {M : Type u} {N : Type v} [] [] (f : M →* N) (x : Mˣ) :
↑(↑() x) = f x
@[simp]
theorem AddUnits.coe_map_neg {M : Type u} {N : Type v} [] [] (f : M →+ N) (u : ) :
↑(-↑() u) = f ↑(-u)
@[simp]
theorem Units.coe_map_inv {M : Type u} {N : Type v} [] [] (f : M →* N) (u : Mˣ) :
(↑() u)⁻¹ = f u⁻¹
@[simp]
theorem AddUnits.map_comp {M : Type u} {N : Type v} {P : Type w} [] [] [] (f : M →+ N) (g : N →+ P) :
@[simp]
theorem Units.map_comp {M : Type u} {N : Type v} {P : Type w} [] [] [] (f : M →* N) (g : N →* P) :
@[simp]
theorem AddUnits.map_id (M : Type u) [] :
@[simp]
theorem Units.map_id (M : Type u) [] :
def AddUnits.coeHom (M : Type u) [] :
→+ M

Coercion AddUnits M → M as an AddMonoid homomorphism.

Instances For
def Units.coeHom (M : Type u) [] :
Mˣ →* M

Coercion Mˣ → M as a monoid homomorphism.

Instances For
@[simp]
theorem AddUnits.coeHom_apply {M : Type u} [] (x : ) :
↑() x = x
@[simp]
theorem Units.coeHom_apply {M : Type u} [] (x : Mˣ) :
↑() x = x
@[simp]
theorem AddUnits.val_nsmul_eq_nsmul_val {M : Type u} [] (u : ) (n : ) :
↑(n u) = n u
@[simp]
theorem Units.val_pow_eq_pow_val {M : Type u} [] (u : Mˣ) (n : ) :
↑(u ^ n) = u ^ n
@[simp]
theorem AddUnits.val_sub_eq_sub_val {α : Type u_1} (u₁ : ) (u₂ : ) :
↑(u₁ - u₂) = u₁ - u₂
@[simp]
theorem Units.val_div_eq_div_val {α : Type u_1} [] (u₁ : αˣ) (u₂ : αˣ) :
↑(u₁ / u₂) = u₁ / u₂
@[simp]
theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} (u : ) (n : ) :
↑(n u) = n u
@[simp]
theorem Units.val_zpow_eq_zpow_val {α : Type u_1} [] (u : αˣ) (n : ) :
↑(u ^ n) = u ^ n
theorem divp_eq_div {α : Type u_1} [] (a : α) (u : αˣ) :
a /ₚ u = a / u
@[simp]
theorem map_addUnits_neg {α : Type u_1} {M : Type u} [] {F : Type u_2} [] (f : F) (u : ) :
f ↑(-u) = -f u
@[simp]
theorem map_units_inv {α : Type u_1} {M : Type u} [] [] {F : Type u_2} [] (f : F) (u : Mˣ) :
f u⁻¹ = (f u)⁻¹
theorem AddUnits.liftRight.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M) (h : ∀ (x : M), ↑(g x) = f x) (x : M) (y : M) :
ZeroHom.toFun { toFun := g, map_zero' := (_ : g 0 = 0) } (x + y) = ZeroHom.toFun { toFun := g, map_zero' := (_ : g 0 = 0) } x + ZeroHom.toFun { toFun := g, map_zero' := (_ : g 0 = 0) } y
theorem AddUnits.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : M) (h : ∀ (x : M), ↑(g x) = f x) :
g 0 = 0
def AddUnits.liftRight {M : Type u} {N : Type v} [] [] (f : M →+ N) (g : M) (h : ∀ (x : M), ↑(g x) = f x) :
M →+

If a map g : M → AddUnits N agrees with a homomorphism f : M →+ N, then this map is an AddMonoid homomorphism too.

Instances For
def Units.liftRight {M : Type u} {N : Type v} [] [] (f : M →* N) (g : MNˣ) (h : ∀ (x : M), ↑(g x) = f x) :
M →* Nˣ

If a map g : M → Nˣ agrees with a homomorphism f : M →* N, then this map is a monoid homomorphism too.

Instances For
@[simp]
theorem AddUnits.coe_liftRight {M : Type u} {N : Type v} [] [] {f : M →+ N} {g : M} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
↑(↑() x) = f x
@[simp]
theorem Units.coe_liftRight {M : Type u} {N : Type v} [] [] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
↑(↑() x) = f x
@[simp]
theorem AddUnits.add_liftRight_neg {M : Type u} {N : Type v} [] [] {f : M →+ N} {g : M} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
f x + ↑(-↑() x) = 0
@[simp]
theorem Units.mul_liftRight_inv {M : Type u} {N : Type v} [] [] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
f x * (↑() x)⁻¹ = 1
@[simp]
theorem AddUnits.liftRight_neg_add {M : Type u} {N : Type v} [] [] {f : M →+ N} {g : M} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
↑(-↑() x) + f x = 0
@[simp]
theorem Units.liftRight_inv_mul {M : Type u} {N : Type v} [] [] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
(↑() x)⁻¹ * f x = 1
theorem AddMonoidHom.toHomAddUnits.proof_3 {G : Type u_2} {M : Type u_1} [] [] (f : G →+ M) :
∀ (x : G), ↑((fun g => { val := f g, neg := f (-g), val_neg := (_ : f g + f (-g) = 0), neg_val := (_ : f (-g) + f g = 0) }) x) = ↑((fun g => { val := f g, neg := f (-g), val_neg := (_ : f g + f (-g) = 0), neg_val := (_ : f (-g) + f g = 0) }) x)
theorem AddMonoidHom.toHomAddUnits.proof_2 {G : Type u_2} {M : Type u_1} [] [] (f : G →+ M) (g : G) :
f (-g) + f g = 0
def AddMonoidHom.toHomAddUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →+ M) :
G →+

If f is a homomorphism from an additive group G to an additive monoid M, then its image lies in the AddUnits of M, and f.toHomUnits is the corresponding homomorphism from G to AddUnits M.

Instances For
theorem AddMonoidHom.toHomAddUnits.proof_1 {G : Type u_2} {M : Type u_1} [] [] (f : G →+ M) (g : G) :
f g + f (-g) = 0
def MonoidHom.toHomUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →* M) :
G →* Mˣ

If f is a homomorphism from a group G to a monoid M, then its image lies in the units of M, and f.toHomUnits is the corresponding monoid homomorphism from G to Mˣ.

Instances For
@[simp]
theorem AddMonoidHom.coe_toHomAddUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →+ M) (g : G) :
↑() = f g
@[simp]
theorem MonoidHom.coe_toHomUnits {G : Type u_1} {M : Type u_2} [] [] (f : G →* M) (g : G) :
↑(↑() g) = f g
theorem IsAddUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [] (f : F) {x : M} (h : ) :
theorem IsUnit.map {F : Type u_1} {M : Type u_4} {N : Type u_5} [] [] [] (f : F) {x : M} (h : ) :
IsUnit (f x)
theorem IsAddUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [] [] {f : F} {x : M} (g : G) (hfg : ) (h : IsAddUnit (f x)) :
theorem IsUnit.of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [] [] {f : F} {x : M} (g : G) (hfg : ) (h : IsUnit (f x)) :
theorem isAddUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [] [] {f : F} {x : M} (g : G) (hfg : ) :
theorem isUnit_map_of_leftInverse {F : Type u_1} {G : Type u_2} {M : Type u_4} {N : Type u_5} [] [] [] [] {f : F} {x : M} (g : G) (hfg : ) :
IsUnit (f x)
noncomputable def IsAddUnit.liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :
M →+

If a homomorphism f : M →+ N sends each element to an IsAddUnit, then it can be lifted to f : M →+ AddUnits N. See also AddUnits.liftRight for a computable version.

Instances For
theorem IsAddUnit.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :
noncomputable def IsUnit.liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) :
M →* Nˣ

If a homomorphism f : M →* N sends each element to an IsUnit, then it can be lifted to f : M →* Nˣ. See also Units.liftRight for a computable version.

Instances For
theorem IsAddUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) (x : M) :
↑(↑() x) = f x
theorem IsUnit.coe_liftRight {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) (x : M) :
↑(↑() x) = f x
@[simp]
theorem IsAddUnit.add_liftRight_neg {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
f x + ↑(-↑() x) = 0
@[simp]
theorem IsUnit.mul_liftRight_inv {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
f x * (↑() x)⁻¹ = 1
@[simp]
theorem IsAddUnit.liftRight_neg_add {M : Type u_4} {N : Type u_5} [] [] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
↑(-↑() x) + f x = 0
@[simp]
theorem IsUnit.liftRight_inv_mul {M : Type u_4} {N : Type u_5} [] [] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
(↑() x)⁻¹ * f x = 1
def IsAddUnit.addUnit' {α : Type u_3} {a : α} (h : ) :

The element of the additive group of additive units, corresponding to an element of an additive monoid which is an additive unit. As opposed to IsAddUnit.addUnit, the negation is computable and comes from the negation on α. This is useful to transfer properties of negation in AddUnits α to α. See also toAddUnits.

Instances For
@[simp]
theorem IsUnit.val_unit' {α : Type u_3} [] {a : α} (h : ) :
↑() = a
@[simp]
theorem IsAddUnit.val_addUnit' {α : Type u_3} {a : α} (h : ) :
↑() = a
def IsUnit.unit' {α : Type u_3} [] {a : α} (h : ) :
αˣ

The element of the group of units, corresponding to an element of a monoid which is a unit. As opposed to IsUnit.unit, the inverse is computable and comes from the inversion on α. This is useful to transfer properties of inversion in Units α to α. See also toUnits.

Instances For
theorem IsAddUnit.val_neg_addUnit' {α : Type u_3} {a : α} (h : ) :
↑() = -a
theorem IsUnit.val_inv_unit' {α : Type u_3} [] {a : α} (h : ) :
()⁻¹ = a⁻¹
@[simp]
theorem IsAddUnit.add_neg_cancel_left {α : Type u_3} {a : α} (h : ) (b : α) :
a + (-a + b) = b
@[simp]
theorem IsUnit.mul_inv_cancel_left {α : Type u_3} [] {a : α} (h : ) (b : α) :
a * (a⁻¹ * b) = b
@[simp]
theorem IsAddUnit.neg_add_cancel_left {α : Type u_3} {a : α} (h : ) (b : α) :
-a + (a + b) = b
@[simp]
theorem IsUnit.inv_mul_cancel_left {α : Type u_3} [] {a : α} (h : ) (b : α) :
a⁻¹ * (a * b) = b
@[simp]
theorem IsAddUnit.add_neg_cancel_right {α : Type u_3} {b : α} (h : ) (a : α) :
a + b + -b = a
@[simp]
theorem IsUnit.mul_inv_cancel_right {α : Type u_3} [] {b : α} (h : ) (a : α) :
a * b * b⁻¹ = a
@[simp]
theorem IsAddUnit.neg_add_cancel_right {α : Type u_3} {b : α} (h : ) (a : α) :
a + -b + b = a
@[simp]
theorem IsUnit.inv_mul_cancel_right {α : Type u_3} [] {b : α} (h : ) (a : α) :
a * b⁻¹ * b = a
theorem IsAddUnit.sub_self {α : Type u_3} {a : α} (h : ) :
a - a = 0
theorem IsUnit.div_self {α : Type u_3} [] {a : α} (h : ) :
a / a = 1
theorem IsAddUnit.eq_add_neg_iff_add_eq {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a = b + -c a + c = b
theorem IsUnit.eq_mul_inv_iff_mul_eq {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a = b * c⁻¹ a * c = b
theorem IsAddUnit.eq_neg_add_iff_add_eq {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a = -b + c b + a = c
theorem IsUnit.eq_inv_mul_iff_mul_eq {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a = b⁻¹ * c b * a = c
theorem IsAddUnit.neg_add_eq_iff_eq_add {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
-a + b = c b = a + c
theorem IsUnit.inv_mul_eq_iff_eq_mul {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a⁻¹ * b = c b = a * c
theorem IsAddUnit.add_neg_eq_iff_eq_add {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a + -b = c a = c + b
theorem IsUnit.mul_inv_eq_iff_eq_mul {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a * b⁻¹ = c a = c * b
theorem IsAddUnit.add_neg_eq_zero {α : Type u_3} {a : α} {b : α} (h : ) :
a + -b = 0 a = b
theorem IsUnit.mul_inv_eq_one {α : Type u_3} [] {a : α} {b : α} (h : ) :
a * b⁻¹ = 1 a = b
theorem IsAddUnit.neg_add_eq_zero {α : Type u_3} {a : α} {b : α} (h : ) :
-a + b = 0 a = b
theorem IsUnit.inv_mul_eq_one {α : Type u_3} [] {a : α} {b : α} (h : ) :
a⁻¹ * b = 1 a = b
theorem IsAddUnit.add_eq_zero_iff_eq_neg {α : Type u_3} {a : α} {b : α} (h : ) :
a + b = 0 a = -b
theorem IsUnit.mul_eq_one_iff_eq_inv {α : Type u_3} [] {a : α} {b : α} (h : ) :
a * b = 1 a = b⁻¹
theorem IsAddUnit.add_eq_zero_iff_neg_eq {α : Type u_3} {a : α} {b : α} (h : ) :
a + b = 0 -a = b
theorem IsUnit.mul_eq_one_iff_inv_eq {α : Type u_3} [] {a : α} {b : α} (h : ) :
a * b = 1 a⁻¹ = b
@[simp]
theorem IsAddUnit.sub_add_cancel {α : Type u_3} {b : α} (h : ) (a : α) :
a - b + b = a
@[simp]
theorem IsUnit.div_mul_cancel {α : Type u_3} [] {b : α} (h : ) (a : α) :
a / b * b = a
@[simp]
theorem IsAddUnit.add_sub_cancel {α : Type u_3} {b : α} (h : ) (a : α) :
a + b - b = a
@[simp]
theorem IsUnit.mul_div_cancel {α : Type u_3} [] {b : α} (h : ) (a : α) :
a * b / b = a
theorem IsAddUnit.add_zero_sub_cancel {α : Type u_3} {a : α} (h : ) :
a + (0 - a) = 0
theorem IsUnit.mul_one_div_cancel {α : Type u_3} [] {a : α} (h : ) :
a * (1 / a) = 1
theorem IsAddUnit.zero_sub_add_cancel {α : Type u_3} {a : α} (h : ) :
0 - a + a = 0
theorem IsUnit.one_div_mul_cancel {α : Type u_3} [] {a : α} (h : ) :
1 / a * a = 1
theorem IsAddUnit.neg {α : Type u_3} {a : α} (h : ) :
theorem IsUnit.inv {α : Type u_3} [] {a : α} (h : ) :
theorem IsAddUnit.sub {α : Type u_3} {a : α} {b : α} (ha : ) (hb : ) :
theorem IsUnit.div {α : Type u_3} [] {a : α} {b : α} (ha : ) (hb : ) :
IsUnit (a / b)
theorem IsAddUnit.sub_left_inj {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a - c = b - c a = b
theorem IsUnit.div_left_inj {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a / c = b / c a = b
theorem IsAddUnit.sub_eq_iff {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a - b = c a = c + b
theorem IsUnit.div_eq_iff {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a / b = c a = c * b
theorem IsAddUnit.eq_sub_iff {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a = b - c a + c = b
theorem IsUnit.eq_div_iff {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a = b / c a * c = b
theorem IsAddUnit.sub_eq_of_eq_add {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a = c + ba - b = c
theorem IsUnit.div_eq_of_eq_mul {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a = c * ba / b = c
theorem IsAddUnit.eq_sub_of_add_eq {α : Type u_3} {a : α} {b : α} {c : α} (h : ) :
a + c = ba = b - c
theorem IsUnit.eq_div_of_mul_eq {α : Type u_3} [] {a : α} {b : α} {c : α} (h : ) :
a * c = ba = b / c
theorem IsAddUnit.sub_eq_zero_iff_eq {α : Type u_3} {a : α} {b : α} (h : ) :
a - b = 0 a = b
theorem IsUnit.div_eq_one_iff_eq {α : Type u_3} [] {a : α} {b : α} (h : ) :
a / b = 1 a = b
theorem IsAddUnit.sub_add_left {α : Type u_3} {a : α} {b : α} (h : ) :
b - (a + b) = 0 - a

The AddGroup version of this lemma is sub_add_cancel''

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

The Group version of this lemma is div_mul_cancel'''

theorem IsAddUnit.add_sub_add_right {α : Type u_3} {c : α} (h : ) (a : α) (b : α) :
a + c - (b + c) = a - b
theorem IsUnit.mul_div_mul_right {α : Type u_3} [] {c : α} (h : ) (a : α) (b : α) :
a * c / (b * c) = a / b
a + b + (0 - b) = a
theorem IsUnit.mul_mul_div {α : Type u_3} [] {b : α} (a : α) (h : ) :
a * b * (1 / b) = a
theorem IsAddUnit.sub_add_right {α : Type u_3} {a : α} (h : ) (b : α) :
a - (a + b) = 0 - b
theorem IsUnit.div_mul_right {α : Type u_3} {a : α} (h : ) (b : α) :
a / (a * b) = 1 / b
theorem IsAddUnit.add_sub_cancel_left {α : Type u_3} {a : α} (h : ) (b : α) :
a + b - a = b
theorem IsUnit.mul_div_cancel_left {α : Type u_3} {a : α} (h : ) (b : α) :
a * b / a = b
theorem IsAddUnit.add_sub_cancel' {α : Type u_3} {a : α} (h : ) (b : α) :
a + (b - a) = b
theorem IsUnit.mul_div_cancel' {α : Type u_3} {a : α} (h : ) (b : α) :
a * (b / a) = b
theorem IsAddUnit.add_sub_add_left {α : Type u_3} {c : α} (h : ) (a : α) (b : α) :
c + a - (c + b) = a - b
theorem IsUnit.mul_div_mul_left {α : Type u_3} {c : α} (h : ) (a : α) (b : α) :
c * a / (c * b) = a / b
theorem IsAddUnit.add_eq_add_of_sub_eq_sub {α : Type u_3} {b : α} {d : α} (hb : ) (hd : ) (a : α) (c : α) (h : a - b = c - d) :
a + d = c + b
theorem IsUnit.mul_eq_mul_of_div_eq_div {α : Type u_3} {b : α} {d : α} (hb : ) (hd : ) (a : α) (c : α) (h : a / b = c / d) :
a * d = c * b
theorem IsAddUnit.sub_eq_sub_iff {α : Type u_3} {a : α} {b : α} {c : α} {d : α} (hb : ) (hd : ) :
a - b = c - d a + d = c + b
theorem IsUnit.div_eq_div_iff {α : Type u_3} {a : α} {b : α} {c : α} {d : α} (hb : ) (hd : ) :
a / b = c / d a * d = c * b
theorem IsAddUnit.sub_sub_cancel {α : Type u_3} {a : α} {b : α} (h : ) :
a - (a - b) = b
theorem IsUnit.div_div_cancel {α : Type u_3} {a : α} {b : α} (h : ) :
a / (a / b) = b
theorem IsAddUnit.sub_sub_cancel_left {α : Type u_3} {a : α} {b : α} (h : ) :
a - b - a = -b
theorem IsUnit.div_div_cancel_left {α : Type u_3} {a : α} {b : α} (h : ) :
a / b / a = b⁻¹