map_injective — Mathlib

English

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

Русский

Если f инъективен, то map f инъективен на множестве многочленов.

LaTeX

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

Lean4

theorem map_injective (hf : Function.Injective f) : Function.Injective (map f : MvPolynomial σ R → MvPolynomial σ S₁) :=
  by
  intro p q h
  simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢
  intro m
  exact hf (h m)

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