fg_of_isUnit

Mathlib.RingTheory.Finiteness.Subalgebra

URI: https://scilib.ai/kg/mathlib#Submodule.fg_of_isUnit

English

If I is an IsUnit submodule of A, then I is finitely generated.

Русский

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

LaTeX

$$$\text{IsUnit } I \Rightarrow I.FG$$$

Lean4

theorem fg_of_isUnit {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] {I : Submodule R A} (hI : IsUnit I) :
    I.FG :=
  fg_unit hI.unit

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru