finrank — Mathlib

English

If StrongRankCondition holds for R, then Module.finrank R S equals pb.dim for pb a PowerBasis R S.

Русский

При заданном сильном ранге для R, размерности модуля: Module.finrank R S = pb.dim для pb — PowerBasis R S.

LaTeX

$$$\\text{finrank}_R(S) = pb.dim$ under $[\\text{StrongRankCondition } R]$ and pb a PowerBasis.$$

Lean4

theorem finrank [StrongRankCondition R] (pb : PowerBasis R S) : Module.finrank R S = pb.dim := by
  rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]

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