Theorem: mem_orthSpace'_iff (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 U : Submodule R (η → R)
l : η →₀ R
⊢ l ∈ U.orthSpace' ↔ ∀ x ∈ U, (Finsupp.total η R R x) l = 0
Tactic:
simp [orthSpace']
State after:
no goals