injective_of_degree_ne_zero — Mathlib

English

If R is a domain and deg f ≠ 0, then AdjoinRoot.of f is injective.

Русский

Если R — домен и deg f ≠ 0, то отображение AdjoinRoot.of f инъективно.

LaTeX

$$$[\\text{IsDomain } R] \\land f.\\deg \\neq 0 \\Rightarrow \\operatorname{Injective}(\\operatorname{AdjoinRoot.of} f)$$$

Lean4

theorem injective_of_degree_ne_zero [IsDomain R] (hf : f.degree ≠ 0) : Function.Injective (AdjoinRoot.of f) :=
  by
  rw [injective_iff_map_eq_zero]
  intro p hp
  rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp
  by_cases h : f = 0
  · exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp))
  · contrapose! hf with h_contra
    rw [← degree_C h_contra]
    apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne, C_eq_zero])) _
    rwa [degree_C h_contra, zero_le_degree_iff]

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