ideal_span_isMaximal_of_prime — Mathlib

English

Let p be a prime number. Then the principal ideal (p) in the integers is a maximal ideal.

Русский

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

LaTeX

$$$\text{Prime}(p) \Rightarrow (p) \text{ maximal in } \mathbb{Z}$$$

Lean4

instance ideal_span_isMaximal_of_prime (p : ℕ) [Fact (Nat.Prime p)] : (Ideal.span {(p : ℤ)}).IsMaximal :=
  Ideal.Quotient.maximal_of_isField _ <| (Int.quotientSpanNatEquivZMod p).toMulEquiv.isField (Field.toIsField _)

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