dual_free — Mathlib

English

For a finite basis b of M, the rank of the dual M is the same as the rank of M, up to a cardinal lifting: rank_R(Dual R M) = lift(rank_R M).

Русский

Для конечного базиса b пространства M ранг дуального равен рангу пространства, с учетом кардинального подъема: rank(Dual M) = lift(rank M).

LaTeX

$$$ \\operatorname{rank}_R(\\mathrm{Dual} \\; R \\; M) = \\mathrm{lift} \\big( \\operatorname{rank}_R M \\big) $$$

Lean4

instance dual_free [Free R M] : Free R (Dual R M) :=
  Free.of_basis (Free.chooseBasis R M).dualBasis

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