prod

Mathlib.RingTheory.FiniteType

URI: https://scilib.ai/kg/mathlib#Algebra.FiniteType.prod

English

If A and B are finitely generated over R, then their direct product A × B is finitely generated over R.

Русский

Если A и B — конечного типа над R, то их прямое произведение A × B также конечного типа над R.

LaTeX

$$FiniteType\\ R\\ A×B$$

Lean4

instance prod [hA : FiniteType R A] [hB : FiniteType R B] : FiniteType R (A × B) :=
  ⟨by rw [← Subalgebra.prod_top]; exact hA.1.prod hB.1⟩

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

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

Разделы

Аффилиация

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