fg_unit — Mathlib

English

If I is a unit in FractionalIdeal S P, then FG (I as a Submodule R P).

Русский

Если I является единичным элементом в FractionalIdeal S P, то I как подмодуль является FG.

LaTeX

$$$ FG (I : Submodule R P) \\quad\\text{for } I \\in (FractionalIdeal S P)^{\\times} $$$

Lean4

theorem fg_unit (I : (FractionalIdeal S P)ˣ) : FG (I : Submodule R P) :=
  Submodule.fg_unit <| Units.map (coeSubmoduleHom S P).toMonoidHom I

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