map_surjective — Mathlib

English

If f is surjective, then map f is surjective on polynomials.

Русский

Если f сюръективен, то map f сюръективно отображает полиномы.

LaTeX

$$$$\text{If } f \text{ is surjective}, \quad \operatorname{map} f \text{ is surjective}. $$$$

Lean4

theorem map_surjective (hf : Function.Surjective f) :
    Function.Surjective (map f : MvPolynomial σ R → MvPolynomial σ S₁) := fun p => by
  induction p using MvPolynomial.induction_on' with
  | monomial i fr =>
    obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  | add a b ha hb =>
    obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, RingHom.map_add _ _ _⟩

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