# Further lemmas about units in a MonoidWithZero or a GroupWithZero. #

theorem Commute.div_eq_div_iff {G₀ : Type u_3} [] {a : G₀} {b : G₀} {c : G₀} {d : G₀} (hbd : Commute b d) (hb : b 0) (hd : d 0) :
a / b = c / d a * d = c * b

The MonoidWithZero version of div_eq_div_iff_mul_eq_mul.

theorem map_ne_zero {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [] [] [] [FunLike 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} [] [] [] [FunLike 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} [] [] [FunLike F' G₀ M₀'] [MonoidWithZeroHomClass F' G₀ M₀'] {a : G₀} (f : F') (g : F') (h : f a = g a) :
f a⁻¹ = g a⁻¹
@[simp]
theorem map_inv₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [] [] [FunLike F G₀ G₀'] [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)⁻¹.

@[simp]
theorem map_div₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [] [] [FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀) (b : G₀) :
f (a / b) = f a / f b
noncomputable def MonoidWithZero.inverse {M : Type u_8} :

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

Equations
• MonoidWithZero.inverse = { toFun := Ring.inverse, map_zero' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem MonoidWithZero.coe_inverse {M : Type u_8} :
MonoidWithZero.inverse = Ring.inverse
@[simp]
theorem MonoidWithZero.inverse_apply {M : Type u_8} (a : M) :
MonoidWithZero.inverse a =
def invMonoidWithZeroHom {G₀ : Type u_8} [] :
G₀ →*₀ G₀

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

Equations
• invMonoidWithZeroHom = let __src := invMonoidHom; { toFun := (__src).toFun, map_zero' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem Units.smul_mk0 {G₀ : Type u_3} [] {α : Type u_8} [SMul G₀ α] {g : G₀} (hg : g 0) (a : α) :
Units.mk0 g hg a = g a
@[simp]
theorem map_zpow₀ {F : Type u_8} {G₀ : Type u_9} {G₀' : Type u_10} [] [] [FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ) :
f (x ^ n) = f x ^ n

If a monoid homomorphism f between two GroupWithZeros maps 0 to 0, then it maps x^n, n : ℤ, to (f x)^n.