quotAnnihilatorEquiv — Mathlib

English

For any finite-dimensional V over K, dim V* = dim V.

Русский

Для конечномерного пространства V над K выполнено: размерность двойственного пространства равна размерности V.

LaTeX

$$finrank K (Module.Dual K V) = finrank K V$$

Lean4

/-- The quotient by the `dualAnnihilator` of a subspace is isomorphic to the
  dual of that subspace. -/
noncomputable def quotAnnihilatorEquiv (W : Subspace K V) :
    (Module.Dual K V ⧸ W.dualAnnihilator) ≃ₗ[K] Module.Dual K W :=
  (quotEquivOfEq _ _ W.dualRestrict_ker_eq_dualAnnihilator).symm.trans <|
    W.dualRestrict.quotKerEquivOfSurjective dualRestrict_surjective

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