of_isNoetherianRing_of_isBezout — Mathlib

English

If S is a principal prime ideal, then its generator is prime.

Русский

Если S — главный простый идеал, то его генератор прост.

LaTeX

$$∀(S: Ideal R) [S.IsPrincipal] [S.IsPrime], Prime (generator S)$$

Lean4

instance (priority := 100) _root_.IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout [IsNoetherianRing R]
    [IsBezout R] : IsPrincipalIdealRing R where principal S := IsBezout.isPrincipal_of_FG S (IsNoetherian.noetherian S)

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