Commit 2024-10-27 10:17 dd8f6e11

View on Github →

feat: add MultilinearMap.dfinsuppFamily and MultilinearMap.piFamily (#17881) This is the analog to Fintype.piFinset Since this is computable and rather confusing, I've included a test with a concrete evaluation.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean

added def MultilinearMap.dfinsuppFamily

added theorem MultilinearMap.dfinsuppFamily_add

added theorem MultilinearMap.dfinsuppFamily_compLinearMap_lsingle

added theorem MultilinearMap.dfinsuppFamily_single

added theorem MultilinearMap.dfinsuppFamily_smul

added theorem MultilinearMap.dfinsuppFamily_zero

added def MultilinearMap.dfinsuppFamilyₗ

added theorem MultilinearMap.support_dfinsuppFamily_subset

Created Mathlib/LinearAlgebra/Multilinear/Pi.lean

added def MultilinearMap.piFamily

added theorem MultilinearMap.piFamily_add

added theorem MultilinearMap.piFamily_compLinearMap_lsingle

added theorem MultilinearMap.piFamily_single

added theorem MultilinearMap.piFamily_smul

added theorem MultilinearMap.piFamily_zero

added def MultilinearMap.piFamilyₗ

Created test/DFinsuppMultiLinear.lean