case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K V
x✝ : { x // x ∈ W }
⊢ ↑(↑(quotAnnihilatorEquiv W) (Submodule.Quotient.mk φ)) x✝ = ↑(↑(dualRestrict W) φ) x✝
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K V
⊢ ↑(quotAnnihilatorEquiv W) (Submodule.Quotient.mk φ) = ↑(dualRestrict W) φ
ext
no goals
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K V
x✝ : { x // x ∈ W }
⊢ ↑(↑(quotAnnihilatorEquiv W) (Submodule.Quotient.mk φ)) x✝ = ↑(↑(dualRestrict W) φ) x✝
rfl