relrank_top_right — Mathlib

English

The relative rank of A over the top subfield equals the rank of E as an A-module.

Русский

Относительный ранг A над верхним подполем равен рангу E как A-модуля.

LaTeX

$$$ \operatorname{relrank}(A,\top) = \operatorname{Module.rank}(A,E)$$$

Lean4

@[simp]
theorem relrank_top_right : relrank A ⊤ = Module.rank A E :=
  by
  let _ : AddCommMonoid (⊤ : IntermediateField A E) := inferInstance
  rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
    IntermediateField.topEquiv.toLinearEquiv.rank_eq]

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