map_eq_zero_iff — Mathlib

English

For a group-with-zero G₀, a nontrivial monoid-with-zero M₀, and a MonoidWithZeroHom f: G₀ →₀ M₀, f(x) = 0 iff x = 0 for all x.

Русский

Для группы с нулём G₀, ненулевого моноида M₀ и MonoidWithZeroHom f: G₀ →₀ M₀ выполняется f(x) = 0 ⇔ x = 0 для всех x.

LaTeX

$$$\forall x,\ f(x) = 0 \iff x = 0$$$

Lean4

protected theorem map_eq_zero_iff {G₀ M₀ : Type*} [GroupWithZero G₀] [MulZeroOneClass M₀] [Nontrivial M₀]
    {f : G₀ →*₀ M₀} {x : G₀} : f x = 0 ↔ x = 0 :=
  by
  refine ⟨?_, by simp +contextual⟩
  contrapose!
  intro hx H
  lift x to G₀ˣ using isUnit_iff_ne_zero.mpr hx
  apply one_ne_zero (α := M₀)
  rw [← map_one f, ← Units.mul_inv x, map_mul, H, zero_mul]

Похожие утверждения