ker_constantCoeff — Mathlib

English

The kernel of the constantCoeff map is the principal ideal generated by X.

Русский

Ядро константного коэффициента равно порождающему идеалу X.

LaTeX

$$$\operatorname{ker}(\operatorname{constantCoeff}) = \langle X \rangle$$$

Lean4

@[simp]
theorem ker_constantCoeff : RingHom.ker constantCoeff = .span {(X : R[X])} :=
  by
  refine le_antisymm (fun p hp ↦ ?_) (by simp [Ideal.span_le])
  simp only [RingHom.mem_ker, constantCoeff_apply, ← Polynomial.X_dvd_iff] at hp
  rwa [Ideal.mem_span_singleton]

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