instCore_1

Mathlib.RingTheory.Extension.Presentation.Core

URI: https://scilib.ai/kg/mathlib#Algebra.Presentation.instCore_1

English

If the indexing set σ is finite, then the core subalgebra P.Core is a finitely generated algebra over the integers ℤ.

Русский

Если множество индексов σ конечное, то ядро P.Core является конечной по типу алгеброй над ℤ.

LaTeX

$$$\\operatorname{FiniteType}_{\\mathbb{Z}}(P^{\\mathrm{Core}})$$$

Lean4

instance : Algebra P.Core S :=
  fast_instance%(inferInstanceAs <| Algebra P.core S)

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

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

Разделы

Аффилиация

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