rank_eq_rank_subalgebra — Mathlib

English

For an intermediate field F of L over K, the K-rank (dimension) of F considered as a subalgebra equals the K-rank of F itself; i.e., rank_K(F as subalgebra) = rank_K(F).

Русский

Для промежуточного поля F внутри L над K размерность F как K-модуль равна размерности F, рассматриваемой как подалгебра.

LaTeX

$$$ \operatorname{rank}_K(F^{\text{toSubalgebra}}) = \operatorname{rank}_K(F) $$$

Lean4

@[simp]
theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F :=
  rfl

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