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]