ker_coeff_eq_max_ideal — Mathlib

English

The kernel of the constant term map on k[[X]] equals the maximal ideal, i.e., all series with zero constant term form the maximal ideal.

Русский

Ядро отображения константного коэффициента в k[[X]] равно максимальному идеалу: все ряды с нулевым константным членом образуют максимальный идеал.

LaTeX

$$\ker(\text{constantCoeff}) = \operatorname{maximalIdeal}(k[[X]])$$

Lean4

theorem ker_coeff_eq_max_ideal : RingHom.ker (constantCoeff (R := k)) = maximalIdeal _ :=
  Ideal.ext fun _ ↦ by rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]

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