finite_bot

Mathlib.RingTheory.Finiteness.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.finite_bot

English

The bottom subalgebra, viewed as a module over R, is finite (finitely generated).

Русский

Нижняя подпалгебра, рассматриваемая как модуль над R, конечно порождается.

LaTeX

$$$(\perp : \text{Subalgebra } R A).toSubmodule \text{ is a finite } R\text{-module}$$$

Lean4

instance finite_bot : Module.Finite R (⊥ : Subalgebra R A) :=
  Module.Finite.range (Algebra.linearMap R A)

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

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

Разделы

Аффилиация

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