coeIdeal_fg — Mathlib

English

Under an injective algebra map, FG of the fractional ideal image equals FG of the original ideal: FG((I : FractionalIdeal S P) : Submodule R P) ↔ I.FG.

Русский

При инъективном алгебраическом отображении FG образа дробного идеала совпадает с FG исходного(I.FG).

LaTeX

$$$ FG\\left( (I : \\mathrm{FractionalIdeal} S P) : \\mathrm{Submodule} \\ R P \\right) \\iff I.FG $$$

Lean4

theorem coeIdeal_fg (inj : Function.Injective (algebraMap R P)) (I : Ideal R) :
    FG ((I : FractionalIdeal S P) : Submodule R P) ↔ I.FG :=
  coeSubmodule_fg _ inj _

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