rank_bot — Mathlib

English

The bottom subalgebra has rank 1.

Русский

Нижняя подалгебра имеет ранг 1.

LaTeX

$$$\operatorname{Module.rank}_F(\bot_{\text{Subalgebra}}) = 1$$$

Lean4

@[simp]
theorem rank_bot : Module.rank F (⊥ : Subalgebra F E) = 1 :=
  (Subalgebra.toSubmoduleEquiv (⊥ : Subalgebra F E)).symm.rank_eq.trans <|
    by
    rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]
    letI := Module.nontrivial F E
    exact LinearIndepOn.id_singleton _ one_ne_zero

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