map_ne_zero — Mathlib

English

Let f be a map that respects multiplication and zero; then f preserves nonzeroness: f a ≠ 0 iff a ≠ 0, provided certain nontriviality hypothesis on the codomain.

Русский

Пусть f сохраняет умножение и ноль; тогда f сохраняет ненулевые элементы: f a ≠ 0 эквивалентно a ≠ 0, при условии не тривиальности кодомона.

LaTeX

$$$\\text{map\_ne\_zero}(f): \\forall a, (f a \\neq 0) \\iff (a \\neq 0)$$$

Lean4

theorem map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
  by
  refine ⟨fun hfa ha => hfa <| ha.symm ▸ map_zero f, ?_⟩
  intro hx H
  lift a to G₀ˣ using isUnit_iff_ne_zero.mpr hx
  apply one_ne_zero (α := M₀')
  rw [← map_one f, ← Units.mul_inv a, map_mul, H, zero_mul]

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