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 #

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 AddGroup.isAddUnit {G : Type u_1} [inst : AddGroup G] (g : G) :
theorem Group.isUnit {G : Type u_1} [inst : Group G] (g : G) :
theorem IsAddUnit.eq_on_neg {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : SubtractionMonoid G] [inst : AddMonoid N] [inst : AddMonoidHomClass F G N] {x : G} (hx : IsAddUnit x) (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} [inst : DivisionMonoid G] [inst : Monoid N] [inst : MonoidHomClass F G N] {x : G} (hx : IsUnit x) (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} [inst : AddGroup G] [inst : AddMonoid M] [inst : AddMonoidHomClass F G M] (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} [inst : Group G] [inst : Monoid M] [inst : MonoidHomClass F G M] (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} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) :

The additive homomorphism on AddUnits induced by an AddMonoidHom.

Equations
  • One or more equations did not get rendered due to their size.
def AddUnits.map.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (x : AddUnits M) (y : AddUnits M) :
(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
Equations
  • One or more equations did not get rendered due to their size.
def AddUnits.map.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (u : AddUnits M) :
f u + f u.neg = 0
Equations
  • (_ : f u + f u.neg = 0) = (_ : f u + f u.neg = 0)
def AddUnits.map.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (u : AddUnits M) :
f u.neg + f u = 0
Equations
  • (_ : f u.neg + f u = 0) = (_ : f u.neg + f u = 0)
def Units.map {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] (f : M →* N) :

The group homomorphism on units induced by a MonoidHom.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddUnits.coe_map {M : Type u} {N : Type v} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (x : AddUnits M) :
↑(↑(AddUnits.map f) x) = f x
@[simp]
theorem Units.coe_map {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (x : Mˣ) :
↑(↑(Units.map f) x) = f x
@[simp]
theorem AddUnits.coe_map_neg {M : Type u} {N : Type v} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (u : AddUnits M) :
↑(-↑(AddUnits.map f) u) = f ↑(-u)
@[simp]
theorem Units.coe_map_inv {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (u : Mˣ) :
(↑(Units.map f) u)⁻¹ = f u⁻¹
@[simp]
theorem AddUnits.map_comp {M : Type u} {N : Type v} {P : Type w} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddMonoid P] (f : M →+ N) (g : N →+ P) :
@[simp]
theorem Units.map_comp {M : Type u} {N : Type v} {P : Type w} [inst : Monoid M] [inst : Monoid N] [inst : Monoid P] (f : M →* N) (g : N →* P) :
@[simp]
theorem Units.map_id (M : Type u) [inst : Monoid M] :
def AddUnits.coeHom (M : Type u) [inst : AddMonoid M] :

Coercion AddUnits M → M→ M as an AddMonoid homomorphism.

Equations
  • AddUnits.coeHom M = { toZeroHom := { toFun := AddUnits.val, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (a b : AddUnits M), ↑(a + b) = a + b) }
def Units.coeHom (M : Type u) [inst : Monoid M] :
Mˣ →* M

Coercion Mˣ → M→ M as a monoid homomorphism.

Equations
  • Units.coeHom M = { toOneHom := { toFun := Units.val, map_one' := (_ : 1 = 1) }, map_mul' := (_ : ∀ (a b : Mˣ), ↑(a * b) = a * b) }
@[simp]
theorem AddUnits.coeHom_apply {M : Type u} [inst : AddMonoid M] (x : AddUnits M) :
↑(AddUnits.coeHom M) x = x
@[simp]
theorem Units.coeHom_apply {M : Type u} [inst : Monoid M] (x : Mˣ) :
↑(Units.coeHom M) x = x
@[simp]
theorem AddUnits.val_nsmul_eq_nsmul_val {M : Type u} [inst : AddMonoid M] (u : AddUnits M) (n : ) :
↑(n u) = n u
@[simp]
theorem Units.val_pow_eq_pow_val {M : Type u} [inst : Monoid M] (u : Mˣ) (n : ) :
↑(u ^ n) = u ^ n
@[simp]
theorem AddUnits.val_sub_eq_sub_val {α : Type u_1} [inst : SubtractionMonoid α] (u₁ : AddUnits α) (u₂ : AddUnits α) :
↑(u₁ - u₂) = u₁ - u₂
@[simp]
theorem Units.val_div_eq_div_val {α : Type u_1} [inst : DivisionMonoid α] (u₁ : αˣ) (u₂ : αˣ) :
↑(u₁ / u₂) = u₁ / u₂
@[simp]
theorem AddUnits.val_zsmul_eq_zsmul_val {α : Type u_1} [inst : SubtractionMonoid α] (u : AddUnits α) (n : ) :
↑(n u) = n u
@[simp]
theorem Units.val_zpow_eq_zpow_val {α : Type u_1} [inst : DivisionMonoid α] (u : αˣ) (n : ) :
↑(u ^ n) = u ^ n
theorem divp_eq_div {α : Type u_1} [inst : DivisionMonoid α] (a : α) (u : αˣ) :
a /ₚ u = a / u
@[simp]
theorem map_addUnits_neg {α : Type u_2} {M : Type u} [inst : AddMonoid M] [inst : SubtractionMonoid α] {F : Type u_1} [inst : AddMonoidHomClass F M α] (f : F) (u : AddUnits M) :
f ↑(-u) = -f u
@[simp]
theorem map_units_inv {α : Type u_2} {M : Type u} [inst : Monoid M] [inst : DivisionMonoid α] {F : Type u_1} [inst : MonoidHomClass F M α] (f : F) (u : Mˣ) :
f u⁻¹ = (f u)⁻¹
def AddUnits.liftRight.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (g : MAddUnits N) (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
Equations
  • One or more equations did not get rendered due to their size.
def AddUnits.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (g : MAddUnits N) (h : ∀ (x : M), ↑(g x) = f x) :
g 0 = 0
Equations
  • (_ : g 0 = 0) = (_ : g 0 = 0)
def AddUnits.liftRight {M : Type u} {N : Type v} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (g : MAddUnits N) (h : ∀ (x : M), ↑(g x) = f x) :

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

Equations
  • One or more equations did not get rendered due to their size.
def Units.liftRight {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (g : MNˣ) (h : ∀ (x : M), ↑(g x) = f x) :
M →* Nˣ

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddUnits.coe_liftRight {M : Type u} {N : Type v} [inst : AddMonoid M] [inst : AddMonoid N] {f : M →+ N} {g : MAddUnits N} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
↑(↑(AddUnits.liftRight f g h) x) = f x
@[simp]
theorem Units.coe_liftRight {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
↑(↑(Units.liftRight f g h) x) = f x
@[simp]
theorem AddUnits.add_liftRight_neg {M : Type u} {N : Type v} [inst : AddMonoid M] [inst : AddMonoid N] {f : M →+ N} {g : MAddUnits N} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
f x + ↑(-↑(AddUnits.liftRight f g h) x) = 0
@[simp]
theorem Units.mul_liftRight_inv {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
f x * (↑(Units.liftRight f g h) x)⁻¹ = 1
@[simp]
theorem AddUnits.liftRight_neg_add {M : Type u} {N : Type v} [inst : AddMonoid M] [inst : AddMonoid N] {f : M →+ N} {g : MAddUnits N} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
↑(-↑(AddUnits.liftRight f g h) x) + f x = 0
@[simp]
theorem Units.liftRight_inv_mul {M : Type u} {N : Type v} [inst : Monoid M] [inst : Monoid N] {f : M →* N} {g : MNˣ} (h : ∀ (x : M), ↑(g x) = f x) (x : M) :
(↑(Units.liftRight f g h) x)⁻¹ * f x = 1
def AddMonoidHom.toHomAddUnits.proof_3 {G : Type u_2} {M : Type u_1} [inst : AddGroup G] [inst : AddMonoid M] (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)
Equations
  • One or more equations did not get rendered due to their size.
def AddMonoidHom.toHomAddUnits.proof_2 {G : Type u_2} {M : Type u_1} [inst : AddGroup G] [inst : AddMonoid M] (f : G →+ M) (g : G) :
f (-g) + f g = 0
Equations
  • (_ : f (-g) + f g = 0) = (_ : f (-g) + f g = 0)
def AddMonoidHom.toHomAddUnits {G : Type u_1} {M : Type u_2} [inst : AddGroup G] [inst : AddMonoid M] (f : G →+ M) :

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.

Equations
  • One or more equations did not get rendered due to their size.
def AddMonoidHom.toHomAddUnits.proof_1 {G : Type u_2} {M : Type u_1} [inst : AddGroup G] [inst : AddMonoid M] (f : G →+ M) (g : G) :
f g + f (-g) = 0
Equations
  • (_ : f g + f (-g) = 0) = (_ : f g + f (-g) = 0)
def MonoidHom.toHomUnits {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] (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 .

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddMonoidHom.coe_toHomAddUnits {G : Type u_1} {M : Type u_2} [inst : AddGroup G] [inst : AddMonoid M] (f : G →+ M) (g : G) :
↑(↑(AddMonoidHom.toHomAddUnits f) g) = f g
@[simp]
theorem MonoidHom.coe_toHomUnits {G : Type u_1} {M : Type u_2} [inst : Group G] [inst : Monoid M] (f : G →* M) (g : G) :
↑(↑(MonoidHom.toHomUnits f) g) = f g
theorem IsAddUnit.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddMonoidHomClass F M N] (f : F) {x : M} (h : IsAddUnit x) :
IsAddUnit (f x)
theorem IsUnit.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] [inst : MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) :
IsUnit (f x)
theorem IsAddUnit.of_leftInverse {F : Type u_1} {G : Type u_4} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddMonoidHomClass F M N] [inst : AddMonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) (h : IsAddUnit (f x)) :
theorem IsUnit.of_leftInverse {F : Type u_1} {G : Type u_4} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] [inst : MonoidHomClass F M N] [inst : MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) :
theorem isAddUnit_map_of_leftInverse {F : Type u_1} {G : Type u_4} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddMonoidHomClass F M N] [inst : AddMonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
theorem isUnit_map_of_leftInverse {F : Type u_1} {G : Type u_4} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] [inst : MonoidHomClass F M N] [inst : MonoidHomClass G N M] {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
IsUnit (f x) IsUnit x
noncomputable def IsAddUnit.liftRight {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :

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

Equations
def IsAddUnit.liftRight.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) :
∀ (x : M), ↑(IsAddUnit.addUnit (hf x)) = ↑(IsAddUnit.addUnit (hf x))
Equations
noncomputable def IsUnit.liftRight {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) :
M →* Nˣ

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

Equations
theorem IsAddUnit.coe_liftRight {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (hf : ∀ (x : M), IsAddUnit (f x)) (x : M) :
↑(↑(IsAddUnit.liftRight f hf) x) = f x
theorem IsUnit.coe_liftRight {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)) (x : M) :
↑(↑(IsUnit.liftRight f hf) x) = f x
@[simp]
theorem IsAddUnit.add_liftRight_neg {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
f x + ↑(-↑(IsAddUnit.liftRight f h) x) = 0
@[simp]
theorem IsUnit.mul_liftRight_inv {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
f x * (↑(IsUnit.liftRight f h) x)⁻¹ = 1
@[simp]
theorem IsAddUnit.liftRight_neg_add {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (h : ∀ (x : M), IsAddUnit (f x)) (x : M) :
↑(-↑(IsAddUnit.liftRight f h) x) + f x = 0
@[simp]
theorem IsUnit.liftRight_inv_mul {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (h : ∀ (x : M), IsUnit (f x)) (x : M) :
(↑(IsUnit.liftRight f h) x)⁻¹ * f x = 1
def IsAddUnit.addUnit' {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :

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.

Equations
@[simp]
theorem IsAddUnit.addUnit'_neg {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
@[simp]
theorem IsUnit.unit'_val {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
↑(IsUnit.unit' h) = a
@[simp]
theorem IsUnit.unit'_inv {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
@[simp]
theorem IsAddUnit.addUnit'_val {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
def IsUnit.unit' {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
αˣ

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.

Equations
@[simp]
theorem IsAddUnit.add_neg_cancel_left {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + (-a + b) = b
@[simp]
theorem IsUnit.mul_inv_cancel_left {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :
a * (a⁻¹ * b) = b
@[simp]
theorem IsAddUnit.neg_add_cancel_left {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
-a + (a + b) = b
@[simp]
theorem IsUnit.inv_mul_cancel_left {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) (b : α) :
a⁻¹ * (a * b) = b
@[simp]
theorem IsAddUnit.add_neg_cancel_right {α : Type u_1} [inst : SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + b + -b = a
@[simp]
theorem IsUnit.mul_inv_cancel_right {α : Type u_1} [inst : DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a * b * b⁻¹ = a
@[simp]
theorem IsAddUnit.neg_add_cancel_right {α : Type u_1} [inst : SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + -b + b = a
@[simp]
theorem IsUnit.inv_mul_cancel_right {α : Type u_1} [inst : DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a * b⁻¹ * b = a
theorem IsAddUnit.sub_self {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
a - a = 0
theorem IsUnit.div_self {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
a / a = 1
theorem IsAddUnit.eq_add_neg_iff_add_eq {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a = b + -c a + c = b
theorem IsUnit.eq_mul_inv_iff_mul_eq {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a = b * c⁻¹ a * c = b
theorem IsAddUnit.eq_neg_add_iff_add_eq {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a = -b + c b + a = c
theorem IsUnit.eq_inv_mul_iff_mul_eq {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a = b⁻¹ * c b * a = c
theorem IsAddUnit.neg_add_eq_iff_eq_add {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit a) :
-a + b = c b = a + c
theorem IsUnit.inv_mul_eq_iff_eq_mul {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit a) :
a⁻¹ * b = c b = a * c
theorem IsAddUnit.add_neg_eq_iff_eq_add {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a + -b = c a = c + b
theorem IsUnit.mul_inv_eq_iff_eq_mul {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a * b⁻¹ = c a = c * b
theorem IsAddUnit.add_neg_eq_zero {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
a + -b = 0 a = b
theorem IsUnit.mul_inv_eq_one {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
a * b⁻¹ = 1 a = b
theorem IsAddUnit.neg_add_eq_zero {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
-a + b = 0 a = b
theorem IsUnit.inv_mul_eq_one {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : IsUnit a) :
a⁻¹ * b = 1 a = b
theorem IsAddUnit.add_eq_zero_iff_eq_neg {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
a + b = 0 a = -b
theorem IsUnit.mul_eq_one_iff_eq_inv {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
a * b = 1 a = b⁻¹
theorem IsAddUnit.add_eq_zero_iff_neg_eq {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
a + b = 0 -a = b
theorem IsUnit.mul_eq_one_iff_inv_eq {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : IsUnit a) :
a * b = 1 a⁻¹ = b
@[simp]
theorem IsAddUnit.sub_add_cancel {α : Type u_1} [inst : SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a - b + b = a
@[simp]
theorem IsUnit.div_mul_cancel {α : Type u_1} [inst : DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a / b * b = a
@[simp]
theorem IsAddUnit.add_sub_cancel {α : Type u_1} [inst : SubtractionMonoid α] {b : α} (h : IsAddUnit b) (a : α) :
a + b - b = a
@[simp]
theorem IsUnit.mul_div_cancel {α : Type u_1} [inst : DivisionMonoid α] {b : α} (h : IsUnit b) (a : α) :
a * b / b = a
theorem IsAddUnit.add_zero_sub_cancel {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
a + (0 - a) = 0
theorem IsUnit.mul_one_div_cancel {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
a * (1 / a) = 1
theorem IsAddUnit.zero_sub_add_cancel {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
0 - a + a = 0
theorem IsUnit.one_div_mul_cancel {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
1 / a * a = 1
theorem IsAddUnit.neg {α : Type u_1} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a) :
theorem IsUnit.inv {α : Type u_1} [inst : DivisionMonoid α] {a : α} (h : IsUnit a) :
theorem IsAddUnit.sub {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (ha : IsAddUnit a) (hb : IsAddUnit b) :
IsAddUnit (a - b)
theorem IsUnit.div {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (ha : IsUnit a) (hb : IsUnit b) :
IsUnit (a / b)
theorem IsAddUnit.sub_left_inj {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a - c = b - c a = b
theorem IsUnit.div_left_inj {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a / c = b / c a = b
theorem IsAddUnit.sub_eq_iff {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a - b = c a = c + b
theorem IsUnit.div_eq_iff {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a / b = c a = c * b
theorem IsAddUnit.eq_sub_iff {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a = b - c a + c = b
theorem IsUnit.eq_div_iff {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a = b / c a * c = b
theorem IsAddUnit.sub_eq_of_eq_add {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit b) :
a = c + ba - b = c
theorem IsUnit.div_eq_of_eq_mul {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit b) :
a = c * ba / b = c
theorem IsAddUnit.eq_sub_of_add_eq {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} {c : α} (h : IsAddUnit c) :
a + c = ba = b - c
theorem IsUnit.eq_div_of_mul_eq {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} {c : α} (h : IsUnit c) :
a * c = ba = b / c
theorem IsAddUnit.sub_eq_zero_iff_eq {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
a - b = 0 a = b
theorem IsUnit.div_eq_one_iff_eq {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
a / b = 1 a = b
theorem IsAddUnit.sub_add_left {α : Type u_1} [inst : SubtractionMonoid α] {a : α} {b : α} (h : IsAddUnit b) :
b - (a + b) = 0 - a
theorem IsUnit.div_mul_left {α : Type u_1} [inst : DivisionMonoid α] {a : α} {b : α} (h : IsUnit b) :
b / (a * b) = 1 / a
theorem IsAddUnit.add_sub_add_right {α : Type u_1} [inst : SubtractionMonoid α] {c : α} (h : IsAddUnit c) (a : α) (b : α) :
a + c - (b + c) = a - b
theorem IsUnit.mul_div_mul_right {α : Type u_1} [inst : DivisionMonoid α] {c : α} (h : IsUnit c) (a : α) (b : α) :
a * c / (b * c) = a / b
theorem IsAddUnit.add_add_sub {α : Type u_1} [inst : SubtractionMonoid α] {b : α} (a : α) (h : IsAddUnit b) :
a + b + (0 - b) = a
theorem IsUnit.mul_mul_div {α : Type u_1} [inst : DivisionMonoid α] {b : α} (a : α) (h : IsUnit b) :
a * b * (1 / b) = a
theorem IsAddUnit.sub_add_right {α : Type u_1} [inst : SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a - (a + b) = 0 - b
theorem IsUnit.div_mul_right {α : Type u_1} [inst : DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a / (a * b) = 1 / b
theorem IsAddUnit.add_sub_cancel_left {α : Type u_1} [inst : SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + b - a = b
theorem IsUnit.mul_div_cancel_left {α : Type u_1} [inst : DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a * b / a = b
theorem IsAddUnit.add_sub_cancel' {α : Type u_1} [inst : SubtractionCommMonoid α] {a : α} (h : IsAddUnit a) (b : α) :
a + (b - a) = b
theorem IsUnit.mul_div_cancel' {α : Type u_1} [inst : DivisionCommMonoid α] {a : α} (h : IsUnit a) (b : α) :
a * (b / a) = b
theorem IsAddUnit.add_sub_add_left {α : Type u_1} [inst : SubtractionCommMonoid α] {c : α} (h : IsAddUnit c) (a : α) (b : α) :
c + a - (c + b) = a - b
theorem IsUnit.mul_div_mul_left {α : Type u_1} [inst : DivisionCommMonoid α] {c : α} (h : IsUnit c) (a : α) (b : α) :
c * a / (c * b) = a / b
theorem IsAddUnit.add_eq_add_of_sub_eq_sub {α : Type u_1} [inst : SubtractionCommMonoid α] {b : α} {d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) (a : α) (c : α) (h : a - b = c - d) :
a + d = c + b
theorem IsUnit.mul_eq_mul_of_div_eq_div {α : Type u_1} [inst : DivisionCommMonoid α] {b : α} {d : α} (hb : IsUnit b) (hd : IsUnit d) (a : α) (c : α) (h : a / b = c / d) :
a * d = c * b
theorem IsAddUnit.sub_eq_sub_iff {α : Type u_1} [inst : SubtractionCommMonoid α] {a : α} {b : α} {c : α} {d : α} (hb : IsAddUnit b) (hd : IsAddUnit d) :
a - b = c - d a + d = c + b
theorem IsUnit.div_eq_div_iff {α : Type u_1} [inst : DivisionCommMonoid α] {a : α} {b : α} {c : α} {d : α} (hb : IsUnit b) (hd : IsUnit d) :
a / b = c / d a * d = c * b
theorem IsAddUnit.sub_sub_cancel {α : Type u_1} [inst : SubtractionCommMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
a - (a - b) = b
theorem IsUnit.div_div_cancel {α : Type u_1} [inst : DivisionCommMonoid α] {a : α} {b : α} (h : IsUnit a) :
a / (a / b) = b
theorem IsAddUnit.sub_sub_cancel_left {α : Type u_1} [inst : SubtractionCommMonoid α] {a : α} {b : α} (h : IsAddUnit a) :
a - b - a = -b
theorem IsUnit.div_div_cancel_left {α : Type u_1} [inst : DivisionCommMonoid α] {a : α} {b : α} (h : IsUnit a) :
a / b / a = b⁻¹