rank_top' — Mathlib

English

Let F ⊆ E be fields with E an algebra over F. Then the F-dimension of the top intermediate field equals the F-dimension of E.

Русский

Пусть F ⊆ E — поля, причем E является расширением F. Тогда размерность E как векторного пространства над F равна размерности верхнего промежуточного поля.

LaTeX

$$$\operatorname{rank}_F\big( (\top : \text{IntermediateField } F E) \big) = \operatorname{rank}_F E$$$

Lean4

@[simp]
theorem rank_top' : Module.rank F (⊤ : IntermediateField F E) = Module.rank F E :=
  rank_top F E

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