mathlib documentation

algebra.group_with_zero.units.lemmas

Further lemmas about units in a monoid_with_zero or a group_with_zero. #

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

@[simp]
theorem div_self {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
a / a = 1
theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a = b * c⁻¹ a * c = b
theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a = b⁻¹ * c b * a = c
theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (ha : a 0) :
a⁻¹ * b = c b = a * c
theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a * b⁻¹ = c a = c * b
theorem mul_inv_eq_one₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a * b⁻¹ = 1 a = b
theorem inv_mul_eq_one₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a 0) :
a⁻¹ * b = 1 a = b
theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a * b = 1 a = b⁻¹
theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a 0) :
a * b = 1 a⁻¹ = b
@[simp]
theorem div_mul_cancel {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (a : G₀) (h : b 0) :
a / b * b = a
@[simp]
theorem mul_div_cancel {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (a : G₀) (h : b 0) :
a * b / b = a
theorem mul_one_div_cancel {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
a * (1 / a) = 1
theorem one_div_mul_cancel {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
1 / a * a = 1
theorem div_left_inj' {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a / c = b / c a = b
theorem div_eq_iff {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a / b = c a = c * b
theorem eq_div_iff {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
c = a / b c * b = a
theorem div_eq_iff_mul_eq {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a / b = c c * b = a
theorem eq_div_iff_mul_eq {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a = b / c a * c = b
theorem div_eq_of_eq_mul {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a = c * b a / b = c
theorem eq_div_of_mul_eq {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a * c = b a = b / c
theorem div_eq_one_iff_eq {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a / b = 1 a = b
theorem div_mul_left {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
b / (a * b) = 1 / a
theorem mul_div_mul_right {G₀ : Type u_3} [group_with_zero G₀] {c : G₀} (a b : G₀) (hc : c 0) :
a * c / (b * c) = a / b
theorem mul_mul_div {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (a : G₀) (hb : b 0) :
a = a * b * (1 / b)
theorem div_div_div_cancel_right {G₀ : Type u_3} [group_with_zero G₀] {b c : G₀} (a : G₀) (hc : c 0) :
a / c / (b / c) = a / b
theorem div_mul_div_cancel {G₀ : Type u_3} [group_with_zero G₀] {b c : G₀} (a : G₀) (hc : c 0) :
a / c * (c / b) = a / b
theorem div_mul_cancel_of_imp {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : b = 0 a = 0) :
a / b * b = a
theorem mul_div_cancel_of_imp {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : b = 0 a = 0) :
a * b / b = a
@[simp]
theorem divp_mk0 {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) {b : G₀} (hb : b 0) :
a /ₚ units.mk0 b hb = a / b
theorem div_mul_right {G₀ : Type u_3} [comm_group_with_zero G₀] {a : G₀} (b : G₀) (ha : a 0) :
a / (a * b) = 1 / b
theorem mul_div_cancel_left_of_imp {G₀ : Type u_3} [comm_group_with_zero G₀] {a b : G₀} (h : a = 0 b = 0) :
a * b / a = b
theorem mul_div_cancel_left {G₀ : Type u_3} [comm_group_with_zero G₀] {a : G₀} (b : G₀) (ha : a 0) :
a * b / a = b
theorem mul_div_cancel_of_imp' {G₀ : Type u_3} [comm_group_with_zero G₀] {a b : G₀} (h : b = 0 a = 0) :
b * (a / b) = a
theorem mul_div_cancel' {G₀ : Type u_3} [comm_group_with_zero G₀] {b : G₀} (a : G₀) (hb : b 0) :
b * (a / b) = a
theorem mul_div_mul_left {G₀ : Type u_3} [comm_group_with_zero G₀] {c : G₀} (a b : G₀) (hc : c 0) :
c * a / (c * b) = a / b
theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_3} [comm_group_with_zero G₀] (a : G₀) {b : G₀} (c : G₀) {d : G₀} (hb : b 0) (hd : d 0) (h : a / b = c / d) :
a * d = c * b
theorem div_eq_div_iff {G₀ : Type u_3} [comm_group_with_zero G₀] {a b c d : G₀} (hb : b 0) (hd : d 0) :
a / b = c / d a * d = c * b
theorem div_div_cancel' {G₀ : Type u_3} [comm_group_with_zero G₀] {a b : G₀} (ha : a 0) :
a / (a / b) = b
theorem div_helper {G₀ : Type u_3} [comm_group_with_zero G₀] {a : G₀} (b : G₀) (h : a 0) :
1 / (a * b) * a = 1 / b
theorem map_ne_zero {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [monoid_with_zero M₀] [group_with_zero G₀] [nontrivial M₀] [monoid_with_zero_hom_class F G₀ M₀] (f : F) {a : G₀} :
f a 0 a 0
@[simp]
theorem map_eq_zero {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [monoid_with_zero M₀] [group_with_zero G₀] [nontrivial M₀] [monoid_with_zero_hom_class F G₀ M₀] (f : F) {a : G₀} :
f a = 0 a = 0
theorem eq_on_inv₀ {G₀ : Type u_3} {M₀' : Type u_4} {F' : Type u_7} [group_with_zero G₀] [monoid_with_zero M₀'] [monoid_with_zero_hom_class F' G₀ M₀'] {a : G₀} (f g : F') (h : f a = g a) :
@[simp]
theorem map_inv₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [group_with_zero G₀] [group_with_zero G₀'] [monoid_with_zero_hom_class F G₀ G₀'] (f : F) (a : G₀) :

A monoid homomorphism between groups with zeros sending 0 to 0 sends a⁻¹ to (f a)⁻¹.

@[simp]
theorem map_div₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [group_with_zero G₀] [group_with_zero G₀'] [monoid_with_zero_hom_class F G₀ G₀'] (f : F) (a b : G₀) :
f (a / b) = f a / f b
noncomputable def monoid_with_zero.inverse {M : Type u_1} [comm_monoid_with_zero M] :

We define the inverse as a monoid_with_zero_hom by extending the inverse map by zero on non-units.

Equations
def inv_monoid_with_zero_hom {G₀ : Type u_1} [comm_group_with_zero G₀] :
G₀ →*₀ G₀

Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.

Equations
@[simp]
theorem units.smul_mk0 {G₀ : Type u_3} [group_with_zero G₀] {α : Type u_1} [has_smul G₀ α] {g : G₀} (hg : g 0) (a : α) :
units.mk0 g hg a = g a