maximalIdeal_eq_span_singleton_eps

English

If K is a field, then the maximal ideal of the dual-number ring K[ε] equals the span of ε, i.e., (ε) is the unique maximal ideal.

Русский

Пусть K — поле. Тогда максимальный идеал кольца двойственных чисел K[ε] равен порожденному ε, то есть (ε) является единственным максимальным идеалом.

LaTeX

$$$\text{IsLocalRing.maximalIdeal}(K[\varepsilon]) = \operatorname{span}\{\varepsilon\}$$$

Lean4

theorem maximalIdeal_eq_span_singleton_eps [Field K] : IsLocalRing.maximalIdeal K[ε] = Ideal.span {ε} :=
  (IsLocalRing.eq_maximalIdeal isMaximal_span_singleton_eps).symm

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