finrank_of_isPerfPair — Mathlib

English

Let p be a perfect pairing between M and N with M finite-free over the ring R. Then finrank_R M = finrank_R N.

Русский

Пусть p — совершенная пара между M и N, причем M является конечновольной (свободной) над R. Тогда finrank_R M = finrank_R N.

LaTeX

$$$\operatorname{finrank}_R M = \operatorname{finrank}_R N$$$

Lean4

theorem _root_.Module.finrank_of_isPerfPair [Module.Finite R M] [Module.Free R M] : finrank R M = finrank R N :=
  ((Module.Free.chooseBasis R M).toDualEquiv.trans p.flip.toPerfPair.symm).finrank_eq

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