one_notMem_ker — Mathlib

English

If the codomain is not the zero ring, then the unit 1 is not in the kernel of f.

Русский

Если кодируемое кольцо не нулевое, то единица 1 не принадлежит ядру f.

LaTeX

$$$1 \\notin \\ker f$ (when the codomain is nontrivial)$$

Lean4

/-- If the target is not the zero ring, then one is not in the kernel. -/
theorem one_notMem_ker [Nontrivial S] (f : F) : (1 : R) ∉ ker f :=
  by
  rw [mem_ker, map_one]
  exact one_ne_zero

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