map_eq_X_pow — Mathlib

English

For a distinguished polynomial g at I, the image f.map(Quotient.mk I) equals X^deg(g) in the quotient ring.

Русский

Для распределённого полинома g в I образ f.map equals X^{deg(g)} в факторкольце.

LaTeX

$$$f.IsDistinguishedAt I \\to f.map (Ideal.Quotient.mk I) = X^{f.natDegree}$$$

Lean4

theorem map_eq_X_pow {f : R[X]} {I : Ideal R} (distinguish : f.IsDistinguishedAt I) :
    f.map (Ideal.Quotient.mk I) = Polynomial.X ^ f.natDegree :=
  by
  ext i
  by_cases ne : i = f.natDegree
  · simp [ne, distinguish.monic]
  · rcases lt_or_gt_of_ne ne with lt | gt
    · simpa [ne, eq_zero_iff_mem] using (distinguish.mem lt)
    · simp [ne, Polynomial.coeff_eq_zero_of_natDegree_lt gt]

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