surjective_iff_ne_zero — Mathlib

English

In a DivisionSemiring R, for any R-module M, a linear map f: M →ₗ[R] R is surjective if and only if f ≠ 0.

Русский

В делящем полем R модуль M; линейное отображение f: M →ₗ[R] R сюръективно тогда и только тогда, когда оно не нуль.

LaTeX

$$$ \mathrm{Surjective}(f) \; \Leftrightarrow \; f \neq 0 $$$

Lean4

theorem surjective_iff_ne_zero [DivisionSemiring R] [Module R M] {f : M →ₗ[R] R} : Function.Surjective f ↔ f ≠ 0 :=
  by
  refine ⟨ne_zero_of_surjective, fun hf z ↦ ?_⟩
  obtain ⟨y, hy⟩ : ∃ y, f y ≠ 0 := by simpa [Ne, LinearMap.ext_iff] using hf
  exact ⟨(z * (f y)⁻¹) • y, by simp [hy]⟩

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