Further lemmas about units in a MonoidWithZero or a GroupWithZero.

ink

@[simp]

theorem div_self {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a / a = 1

ink

theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c ≠ 0) : a = b * c⁻¹ ↔ a * c = b

ink

theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b ≠ 0) : a = b⁻¹ * c ↔ b * a = c

ink

theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (ha : a ≠ 0) : a⁻¹ * b = c ↔ b = a * c

ink

theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b ≠ 0) : a * b⁻¹ = c ↔ a = c * b

ink

theorem mul_inv_eq_one₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b ≠ 0) : a * b⁻¹ = 1 ↔ a = b

ink

theorem inv_mul_eq_one₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a ≠ 0) : a⁻¹ * b = 1 ↔ a = b

ink

theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b ≠ 0) : a * b = 1 ↔ a = b⁻¹

ink

theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (ha : a ≠ 0) : a * b = 1 ↔ a⁻¹ = b

ink

@[simp]

theorem div_mul_cancel {G₀ : Type u_1} [inst : GroupWithZero G₀] {b : G₀} (a : G₀) (h : b ≠ 0) : a / b * b = a

ink

@[simp]

theorem mul_div_cancel {G₀ : Type u_1} [inst : GroupWithZero G₀] {b : G₀} (a : G₀) (h : b ≠ 0) : a * b / b = a

ink

theorem mul_one_div_cancel {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a * (1 / a) = 1

ink

theorem one_div_mul_cancel {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : 1 / a * a = 1

ink

theorem div_left_inj' {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c ≠ 0) : a / c = b / c ↔ a = b

ink

theorem div_eq_iff {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b ≠ 0) : a / b = c ↔ a = c * b

ink

theorem eq_div_iff {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b ≠ 0) : c = a / b ↔ c * b = a

ink

theorem div_eq_iff_mul_eq {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b ≠ 0) : a / b = c ↔ c * b = a

ink

theorem eq_div_iff_mul_eq {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c ≠ 0) : a = b / c ↔ a * c = b

ink

theorem div_eq_of_eq_mul {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hb : b ≠ 0) : a = c * b → a / b = c

ink

theorem eq_div_of_mul_eq {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hc : c ≠ 0) : a * c = b → a = b / c

ink

theorem div_eq_one_iff_eq {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b ≠ 0) : a / b = 1 ↔ a = b

ink

theorem div_mul_left {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (hb : b ≠ 0) : b / (a * b) = 1 / a

ink

theorem mul_div_mul_right {G₀ : Type u_1} [inst : GroupWithZero G₀] {c : G₀} (a : G₀) (b : G₀) (hc : c ≠ 0) : a * c / (b * c) = a / b

ink

theorem mul_mul_div {G₀ : Type u_1} [inst : GroupWithZero G₀] {b : G₀} (a : G₀) (hb : b ≠ 0) : a = a * b * (1 / b)

ink

theorem div_div_div_cancel_right {G₀ : Type u_1} [inst : GroupWithZero G₀] {b : G₀} {c : G₀} (a : G₀) (hc : c ≠ 0) : a / c / (b / c) = a / b

ink

theorem div_mul_div_cancel {G₀ : Type u_1} [inst : GroupWithZero G₀] {b : G₀} {c : G₀} (a : G₀) (hc : c ≠ 0) : a / c * (c / b) = a / b

ink

theorem div_mul_cancel_of_imp {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (h : b = 0 → a = 0) : a / b * b = a

ink

theorem mul_div_cancel_of_imp {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (h : b = 0 → a = 0) : a * b / b = a

ink

@[simp]

theorem divp_mk0 {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) {b : G₀} (hb : b ≠ 0) : a /ₚ Units.mk0 b hb = a / b

ink

theorem div_mul_right {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} (b : G₀) (ha : a ≠ 0) : a / (a * b) = 1 / b

ink

theorem mul_div_cancel_left_of_imp {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} {b : G₀} (h : a = 0 → b = 0) : a * b / a = b

ink

theorem mul_div_cancel_left {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} (b : G₀) (ha : a ≠ 0) : a * b / a = b

ink

theorem mul_div_cancel_of_imp' {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} {b : G₀} (h : b = 0 → a = 0) : b * (a / b) = a

ink

theorem mul_div_cancel' {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {b : G₀} (a : G₀) (hb : b ≠ 0) : b * (a / b) = a

ink

theorem mul_div_mul_left {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {c : G₀} (a : G₀) (b : G₀) (hc : c ≠ 0) : c * a / (c * b) = a / b

ink

theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_1} [inst : CommGroupWithZero G₀] (a : G₀) {b : G₀} (c : G₀) {d : G₀} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) : a * d = c * b

ink

theorem div_eq_div_iff {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} {d : G₀} (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b

ink

theorem div_div_cancel' {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} {b : G₀} (ha : a ≠ 0) : a / (a / b) = b

ink

theorem div_div_cancel_left' {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} {b : G₀} (ha : a ≠ 0) : a / b / a = b⁻¹

ink

theorem div_helper {G₀ : Type u_1} [inst : CommGroupWithZero G₀] {a : G₀} (b : G₀) (h : a ≠ 0) : 1 / (a * b) * a = 1 / b

ink

theorem map_ne_zero {M₀ : Type u_1} {G₀ : Type u_3} {F : Type u_2} [inst : MonoidWithZero M₀] [inst : GroupWithZero G₀] [inst : Nontrivial M₀] [inst : MonoidWithZeroHomClass F G₀ M₀] (f : F) {a : G₀} : ↑f a ≠ 0 ↔ a ≠ 0

ink

@[simp]

theorem map_eq_zero {M₀ : Type u_1} {G₀ : Type u_3} {F : Type u_2} [inst : MonoidWithZero M₀] [inst : GroupWithZero G₀] [inst : Nontrivial M₀] [inst : MonoidWithZeroHomClass F G₀ M₀] (f : F) {a : G₀} : ↑f a = 0 ↔ a = 0

ink

theorem eq_on_inv₀ {G₀ : Type u_3} {M₀' : Type u_1} {F' : Type u_2} [inst : GroupWithZero G₀] [inst : MonoidWithZero M₀'] [inst : MonoidWithZeroHomClass F' G₀ M₀'] {a : G₀} (f : F') (g : F') (h : ↑f a = ↑g a) : ↑f a⁻¹ = ↑g a⁻¹

ink

@[simp]

theorem map_inv₀ {G₀ : Type u_2} {G₀' : Type u_1} {F : Type u_3} [inst : GroupWithZero G₀] [inst : GroupWithZero G₀'] [inst : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀) : ↑f a⁻¹ = (↑f a)⁻¹

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

ink

@[simp]

theorem map_div₀ {G₀ : Type u_2} {G₀' : Type u_1} {F : Type u_3} [inst : GroupWithZero G₀] [inst : GroupWithZero G₀'] [inst : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀) (b : G₀) : ↑f (a / b) = ↑f a / ↑f b

ink

noncomputable def MonoidWithZero.inverse {M : Type u_1} [inst : CommMonoidWithZero M] : M →*₀ M

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem MonoidWithZero.coe_inverse {M : Type u_1} [inst : CommMonoidWithZero M] : ↑MonoidWithZero.inverse = Ring.inverse

ink

@[simp]

theorem MonoidWithZero.inverse_apply {M : Type u_1} [inst : CommMonoidWithZero M] (a : M) : ↑MonoidWithZero.inverse a = Ring.inverse a

ink

def invMonoidWithZeroHom {G₀ : Type u_1} [inst : CommGroupWithZero G₀] : G₀ →*₀ G₀

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Units.smul_mk0 {G₀ : Type u_2} [inst : GroupWithZero G₀] {α : Type u_1} [inst : SMul G₀ α] {g : G₀} (hg : g ≠ 0) (a : α) : Units.mk0 g hg • a = g • a