Theorem Finsupp.linearCombination_linear_comp

Modification history

2024-11-13 19:26
Mathlib/LinearAlgebra/Finsupp.lean
chore(LinearAlgebra/Finsupp): split Finsupp.lean into many smaller files (#18869) …
Modified Finsupp.linearCombination_linear_compView on Github →
2024-11-01 08:12
Mathlib/LinearAlgebra/Finsupp.lean
chore: add a helper lemma for `linearCombination` (#18492)
Added Finsupp.linearCombination_linear_compView on Github →