span_maximal_of_irreducible — Mathlib

English

If f is an irreducible polynomial in K[X] over a field K, then the principal ideal generated by f is a maximal ideal of the polynomial ring K[X].

Русский

Если f — irreducible в K[X], то порожденный f основной идеал является максимальным в кольце K[X].

LaTeX

$$\\operatorname{Irreducible}(f) \\Rightarrow (f) \\text{ is maximal in } K[X]$$

Lean4

instance span_maximal_of_irreducible [Fact (Irreducible f)] : (span { f }).IsMaximal :=
  PrincipalIdealRing.isMaximal_of_irreducible <| Fact.out

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