finrank_top' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem finrank_top' : finrank F (⊤ : IntermediateField F E) = finrank F E :=
  finrank_top F E

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