fg_bot_toSubmodule — Mathlib

English

The underlying submodule of the bottom subalgebra is finitely generated; in particular, it is generated by the single element 1.

Русский

Подмодульность нижней подпалгебры является конечно порождаемой; в частности, он порождается элементом 1.

LaTeX

$$$\exists T \subseteq A\, (T \text{ finite}) \text{ such that } \operatorname{span}_R(T) = (\perp : \text{Subalgebra } R A).toSubmodule,$$$

Lean4

theorem fg_bot_toSubmodule : (⊥ : Subalgebra R A).toSubmodule.FG :=
  ⟨{ 1 }, by simp [Algebra.toSubmodule_bot, one_eq_span]⟩

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