Theorem Finsupp.span_single_eq_top

Modification history

2026-02-26 23:39
Mathlib/LinearAlgebra/Finsupp/Span.lean
feat(LinearAlgebra/Finsupp): add lemmas about `lsum` and submodule (#35660) …
Added Finsupp.span_single_eq_topView on Github →