Theorem: orthSpace_top (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : 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 ⊤ = ⊥
Tactic:
rw [orthSpace_eq]
State after:
α : 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 ⊤) = ⊥

State before:
α : 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 ⊤) = ⊥
Tactic:
simp
State after:
no goals