Theorem Finsupp.sum_smul_index_semilinearMap'

Modification history

2025-05-07 05:57
Mathlib/LinearAlgebra/Finsupp/LSum.lean
chore: start semilinearizing LinearAlgebra.Finsupp (#24170)
Added Finsupp.sum_smul_index_semilinearMap'View on Github →