fg_of_isUnit — Mathlib

English

If an ideal I becomes a unit in FractionalIdeal, then I is finitely generated as a submodule.

Русский

Если идеал I становится единицей в дробном идеале, то I конечнопороджен как подсистем.

LaTeX

$$$ FG (I : Submodule R P) $$$

Lean4

theorem _root_.Ideal.fg_of_isUnit (inj : Function.Injective (algebraMap R P)) (I : Ideal R)
    (h : IsUnit (I : FractionalIdeal S P)) : I.FG :=
  by
  rw [← coeIdeal_fg S inj I]
  exact FractionalIdeal.fg_of_isUnit (R := R) I h

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