finrank — Mathlib

English

If R is a division ring and H is a finite-dimensional free R-module, then the finite dimension over R of H and H^{op} coincide: finrank_R(H^{op}) = finrank_R(H).

Русский

Если R — делительное кольцо и H — конечномерный свободный R-модуль, то финитная размерность H и H^{op} совпадают.

LaTeX

$$\operatorname{finrank}_R(H^{\mathrm{op}}) = \operatorname{finrank}_R(H)$$

Lean4

theorem finrank [DivisionRing R] [AddCommGroup H] [Module R H] : Module.finrank R Hᵐᵒᵖ = Module.finrank R H :=
  by
  let b := Basis.ofVectorSpace R H
  rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b.mulOpposite]

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