map_surjective — Mathlib

English

If f is surjective as a ring homomorphism, then the induced map on polynomials p ↦ p.map f is surjective.

Русский

Если gомоморфизм f сюрьективен, то отображение на многочленах p ↦ p.map f сюрьективно.

LaTeX

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

Lean4

theorem map_surjective (hf : Function.Surjective f) : Function.Surjective (map f) := fun p =>
  p.induction_on' (by rintro _ _ ⟨p, rfl⟩ ⟨q, rfl⟩; exact ⟨p + q, Polynomial.map_add f⟩) fun n s ↦
    let ⟨r, hr⟩ := hf s
    ⟨monomial n r, by rw [map_monomial f, hr]⟩

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