subalgebra_top_finrank_eq_submodule_top_finrank

English

The top subalgebra and top submodule have equal finrank.

Русский

У верхней подалгебры и верхнего подмодуля одинаковая финразмерность.

LaTeX

$$$\operatorname{finrank}_F(\top_{\text{Subalgebra}}) = \operatorname{finrank}_F(\top_{\text{Submodule}})$$$

Lean4

theorem subalgebra_top_finrank_eq_submodule_top_finrank :
    finrank F (⊤ : Subalgebra F E) = finrank F (⊤ : Submodule F E) :=
  by
  rw [← Algebra.top_toSubmodule]
  rfl

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