mul

Mathlib.RingTheory.Finiteness.Subalgebra

URI: https://scilib.ai/kg/mathlib#Submodule.FG.mul

English

If M and N are finitely generated submodules, their product M·N is finitely generated.

Русский

Если M и N — конечно порождаемые подмодули, то произведение M·N тоже конечно порождаемо.

LaTeX

$$$M.FG \land N.FG \Rightarrow (M \cdot N).FG$$$

Lean4

theorem mul (hm : M.FG) (hn : N.FG) : (M * N).FG := by rw [mul_eq_map₂]; exact hm.map₂ _ hn

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

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

Разделы

Аффилиация

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