of_injective — Mathlib

English

If f is injective and a is nonzero, then f(a) is nonzero whenever NeZero a holds.

Русский

Если f инъективно отображает, и a ненулевой, то f(a) ненулево, когда a ненулевой.

LaTeX

$$$\\text{hf} : \\text{Injective } f \\Rightarrow (NeZero a \\Rightarrow NeZero (f a))$$$

Lean4

theorem of_injective {f : F} (hf : Injective f) [NeZero a] : NeZero (f a) :=
  ⟨by rw [← ZeroHomClass.map_zero f]; exact hf.ne NeZero.out⟩

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