simp [orthSpace']
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝ : CommRing R
x : η → R
U✝ V U : Submodule R (η → R)
l : η →₀ R
⊢ l ∈ U.orthSpace' ↔ ∀ x ∈ U, (Finsupp.total η R R x) l = 0
no goals