coeSubmodule_isPrincipal — Mathlib

English

Let R be a commutative semiring, K a fraction ring of R, and I an ideal of R. The extension of I to K is principal in K if and only if I is principal in R.

Русский

Пусть R — коммутативное полукольцо, K — дробное кольцо R и I — идеал R. Расширение I в K является главным в K тогда и только тогда, когда I является главным идеалом в R.

LaTeX

$$$ (I K) \,\text{is principal in } K \iff I \text{ is principal in } R $$$

Lean4

@[simp]
theorem coeSubmodule_isPrincipal {I : Ideal R} : (coeSubmodule K I).IsPrincipal ↔ I.IsPrincipal :=
  IsLocalization.coeSubmodule_isPrincipal _ le_rfl

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