subalgebra_top_rank_eq_submodule_top_rank

English

The rank of the top subalgebra equals the rank of the top submodule.

Русский

Ранг верхнего подалгебры равен рангу верхнего подмодуля.

LaTeX

$$$\operatorname{Module.rank}_F(\top_{\text{Subalgebra}}) = \operatorname{Module.rank}_F(\top_{\text{Submodule}})$$$

Lean4

theorem subalgebra_top_rank_eq_submodule_top_rank :
    Module.rank F (⊤ : Subalgebra F E) = Module.rank F (⊤ : Submodule F E) :=
  by
  rw [← Algebra.top_toSubmodule]
  rfl

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