annihilator_le_of_surjective — Mathlib

English

ker f = ⊥ if and only if ∀ x, f(x) = 0 → x = 0.

Русский

ker f = ⊥ если и только если ∀ x, f(x) = 0 ⇒ x = 0.

LaTeX

$$$\\ker f = \\{0\\} \\iff \\forall x (f(x) = 0 \\rightarrow x = 0)$$$

Lean4

theorem annihilator_le_of_surjective (f : M →ₗ[R] M') (hf : Function.Surjective f) :
    Module.annihilator R M ≤ Module.annihilator R M' := fun x h ↦
  by
  rw [Module.mem_annihilator] at h ⊢
  intro m; obtain ⟨m, rfl⟩ := hf m
  rw [← map_smul, h, f.map_zero]

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