relfinrank_top_right — Mathlib

English

The relative finite rank of A over the top subfield equals the finite rank of A over E.

Русский

Относительная конечная размерность A над верхним подполем равна конечной размерности A над E.

LaTeX

$$$ \operatorname{relfinrank}(A,\top) = \operatorname{finrank}(A,E)$$$

Lean4

@[simp]
theorem relfinrank_top_right : relfinrank A ⊤ = finrank A E := by simp [relfinrank_eq_toNat_relrank, finrank]

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