dual_finrank_eq — Mathlib

English

Dimensional equality: dim V* = dim V for finite-dimensional V.

Русский

Равенство размерностей: dim V* = dim V для конечнодименсионального V.

LaTeX

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

Lean4

@[simp]
theorem dual_finrank_eq : finrank K (Module.Dual K V) = finrank K V :=
  by
  by_cases h : FiniteDimensional K V
  · classical exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm
  rw [finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_false]
  · exact fun _ b ↦ h (Module.Finite.of_basis b)
  · exact fun _ b ↦ h ((Module.finite_dual_iff K).mp <| Module.Finite.of_basis b)

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