small

Mathlib.RingTheory.Finiteness.Small

URI: https://scilib.ai/kg/mathlib#Subalgebra.FG.small

← MathLib Explorer

English

If A is a subalgebra of S and A is finitely generated, then A is small.

Русский

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

LaTeX

$$$Small(A) \text{ for } A \text{ FG subalgebra}$$$

Lean4

theorem _root_.Subalgebra.FG.small [Small.{u} R] {A : Subalgebra R S} (fgS : A.FG) : Small.{u} A :=
  by
  obtain ⟨s, hs, rfl⟩ := fgS
  exact small_adjoin

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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