English
Let K be a field and V a finite-dimensional vector space over K. For a subspace W of V*, the dual coannihilator W.dualCoannihilator is a subspace of V consisting of those vectors that are annihilated by every functional in W. Then the sum of the dimensions satisfies dim_K(W) + dim_K(W.dualCoannihilator) = dim_K(V).
Русский
Пусть K — поле, V — конечномерное пространство над K, и W — подпространство V*; тогда W.dualCoannihilator = { v ∈ V : φ(v) = 0 для всех φ ∈ W }. Тогда dim_K(W) + dim_K(W.dualCoannihilator) = dim_K(V).
LaTeX
$$$\\operatorname{finrank}_K(W) + \\operatorname{finrank}_K(W.dualCoannihilator) = \\operatorname{finrank}_K(V)$$$
Lean4
theorem finrank_add_finrank_dualCoannihilator_eq (W : Subspace K (Module.Dual K V)) :
finrank K W + finrank K W.dualCoannihilator = finrank K V := by
rw [finrank_dualCoannihilator_eq, finrank_add_finrank_dualAnnihilator_eq, dual_finrank_eq]
