finrank_dualCoannihilator_eq — Mathlib

English

For Φ ⊆ V*, finite-dimensional setting implies equal finite ranks of Φ.dualCoannihilator and Φ.dualAnnihilator.

Русский

Для подпространства Φ ⊆ V* в конечномерном случае равны размерности Φ.dualCoannihilator и Φ.dualAnnihilator.

LaTeX

$$finrank K Φ.dualCoannihilator = finrank K Φ.dualAnnihilator$$

Lean4

@[simp]
theorem finrank_dualCoannihilator_eq {Φ : Subspace K (Module.Dual K V)} :
    finrank K Φ.dualCoannihilator = finrank K Φ.dualAnnihilator :=
  by
  rw [Submodule.dualCoannihilator, ← Module.evalEquiv_toLinearMap]
  exact LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)

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