map_injective — Mathlib

English

If f: R → S is an injective ring homomorphism, then the induced map on polynomials p ↦ p.map f is injective.

Русский

Если f: R → S — инъективный гомоморфизм колец, то индуцированное отображение на многочленах p ↦ p.map f инъективно.

LaTeX

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

Lean4

theorem map_injective (hf : Function.Injective f) : Function.Injective (map f) := fun p q h =>
  ext fun m => hf <| by rw [← coeff_map f, ← coeff_map f, h]

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