dual_rank_eq — Mathlib

English

If M is a free R-module, then its dual dual(R,M) is also free over R.

Русский

Если M свободный модуль над R, то его дуальное пространство также свободно над R.

LaTeX

$$$ [\\text{Module.Free } R M] \\Rightarrow [\\text{Free } R (\\mathrm{Dual} \\; R \\; M)] $$$

Lean4

theorem dual_rank_eq (b : Basis ι R M) : Module.rank R (Dual R M) = Cardinal.lift.{uR, uM} (Module.rank R M) := by
  classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]

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