Commit 2025-05-07 05:57 e2029bd6

View on Github →

chore: start semilinearizing LinearAlgebra.Finsupp (#24170)

Estimated changes

Modified Mathlib/Data/Finsupp/SMulWithZero.lean

added theorem Finsupp.mapRange_smul'

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

modified theorem Finsupp.lhom_ext'

modified theorem Finsupp.lhom_ext

modified def Finsupp.mapRange.linearEquiv

modified theorem Finsupp.mapRange.linearEquiv_symm

modified theorem Finsupp.mapRange.linearEquiv_toAddEquiv

modified theorem Finsupp.mapRange.linearEquiv_toLinearMap

modified theorem Finsupp.mapRange.linearEquiv_trans

modified def Finsupp.mapRange.linearMap

modified theorem Finsupp.mapRange.linearMap_comp

modified theorem Finsupp.mapRange.linearMap_toAddMonoidHom

Modified Mathlib/LinearAlgebra/Finsupp/LSum.lean

modified theorem Finsupp.coe_lsum

modified def Finsupp.lcongr

modified theorem Finsupp.lcongr_apply_apply

modified theorem Finsupp.lcongr_single

modified theorem Finsupp.lcongr_symm

modified theorem Finsupp.lcongr_symm_single

modified def Finsupp.lsum

modified theorem Finsupp.lsum_apply

modified theorem Finsupp.lsum_comp_lsingle

modified theorem Finsupp.lsum_single

modified theorem Finsupp.lsum_symm_apply

added theorem Finsupp.sum_smul_index_semilinearMap'