Skip to content

feat(LInearAlgebra): predicate version of mem_span_iff_linearCombination#41223

Open
YaelDillies wants to merge 1 commit into
leanprover-community:masterfrom
YaelDillies:mem_span_set_of
Open

feat(LInearAlgebra): predicate version of mem_span_iff_linearCombination#41223
YaelDillies wants to merge 1 commit into
leanprover-community:masterfrom
YaelDillies:mem_span_set_of