finrank_eq — Mathlib

English

If p is a perfect pairing between finite R-modules M and N, then finrank_R(M) = finrank_R(N).

Русский

Если p образует идеальную пару между конечнопериодическими модулями M и N над R, то размерности finrank совпадают.

LaTeX

$$$[ \text{Module.Finite } R M] \land [ \text{Module.Free } R M] \implies \mathrm{finrank}_R(M) = \mathrm{finrank}_R(N).$$$

Lean4

@[deprecated Module.finrank_of_isPerfPair (since := "2025-05-27")]
theorem finrank_eq [Module.Finite R M] [Module.Free R M] : finrank R M = finrank R N :=
  ((Module.Free.chooseBasis R M).toDualEquiv.trans p.toDualRight.symm).finrank_eq

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