of_isPrincipalIdealRing — Mathlib

English

If R is a principal ideal ring, then R is Bezout (every finitely generated ideal is principal).

Русский

Если R — кольцо главных идеалов, то R — Безоу (каждая конечно порожденная идеал — главный).

LaTeX

$$$[IsPrincipalIdealRing R] \Rightarrow IsBezout R$$$

Lean4

instance (priority := 100) of_isPrincipalIdealRing [IsPrincipalIdealRing R] : IsBezout R :=
  ⟨fun I _ => IsPrincipalIdealRing.principal I⟩

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