K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type ?u.1339846
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
Φ : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ comap (↑(Module.evalEquiv K V)) (dualAnnihilator Φ) } = finrank K { x // x ∈ dualAnnihilator Φ }
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type ?u.1339846
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
Φ : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ dualCoannihilator Φ } = finrank K { x // x ∈ dualAnnihilator Φ }
rw [Submodule.dualCoannihilator, ← Module.evalEquiv_toLinearMap]
no goals
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type ?u.1339846
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
Φ : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ comap (↑(Module.evalEquiv K V)) (dualAnnihilator Φ) } = finrank K { x // x ∈ dualAnnihilator Φ }
exact LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)