map_surjective_iff — Mathlib

English

The map on polynomials is surjective iff the base map f on coefficients is surjective: map_surjective_iff.

Русский

Отображение полиномов сюръективно тогда и только тогда, когда отображение коэффициентов f сюръективно: map_surjective_iff.

LaTeX

$$$\\text{Surjective}(\\mathrm{map}\, f) \\iff \\text{Surjective}(f)$$$

Lean4

theorem map_surjective_iff : Function.Surjective (map f) ↔ Function.Surjective f :=
  ⟨fun h s ↦
    let ⟨p, h⟩ := h (C s);
    ⟨p.coeff 0, by simpa using congr(coeff $h 0)⟩,
    map_surjective f⟩

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