English
Let φ be a monoid-with-zero homomorphism between MulZeroOneClass types M₀ and N₀. Under the standing hypotheses that M₀ is Nontrivial and NoZeroDivisors and N₀ is Nontrivial, we have that φ(x) = 1 if and only if x ≠ 0 for every x ∈ M₀. In particular, the only elements mapped to 1 are precisely the nonzero elements.
Русский
Пусть φ — гомоморфизм моноидов с нулём между типами M₀ и N₀. При предположениях, что M₀ ненулевой и не имеет нулевых делителей, а N₀ ненулевой, для любого x ∈ M₀ выполнение φ(x) = 1 тогда и только тогда, когда x ≠ 0. Иными словами, единственными элементами, картографируемыми в 1, являются ненулевые элементы.
LaTeX
$$$ \forall x : M_0,\ (1 : M_0 \to_*_0 N_0)\,x = 1 \ \iff\ x \neq 0. $$$
Lean4
@[simp]
theorem one_apply_eq_one_iff {M₀ N₀ : Type*} [MulZeroOneClass M₀] [MulZeroOneClass N₀]
[DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] [Nontrivial N₀] {x : M₀} :
(1 : M₀ →*₀ N₀) x = 1 ↔ x ≠ 0 := by rcases eq_or_ne x 0 with rfl | hx <;> simp_all [one_apply_of_ne_zero]
