rw [orthSpace_eq]
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ orthSpace ⊤ = ⊥
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝² : CommRing R
x : η → R
U✝ V✝ : Submodule R (η → R)
K : Type u_6
inst✝¹ : Field K
inst✝ : Fintype η
U V : Subspace K (η → K)
⊢ map (Module.piEquiv η K K).symm (dualAnnihilator ⊤) = ⊥