Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.span_eq_span

Modification history

2022-06-16 19:20
src/linear_algebra/span.lean
feat(analysis/inner_product_space): Gram-Schmidt Basis (#14514) …
Added submodule.span_eq_spanView on Github →