Finsupp

📁 Source: Mathlib/LinearAlgebra/Multilinear/Finsupp.lean

Statistics

Metric	Count
Definitions freeFinsuppEquiv	1
Theorems freeFinsuppEquiv_apply, freeFinsuppEquiv_def, freeFinsuppEquiv_single	3
Total	4

MultilinearMap

Definitions

Name	Category	Theorems
freeFinsuppEquiv 📖	CompOp	3 math math: freeFinsuppEquiv_def, freeFinsuppEquiv_apply, freeFinsuppEquiv_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeFinsuppEquiv_apply 📖	mathematical	—	DFunLike.coe MultilinearMap Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule instFunLikeForall LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid instModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv freeFinsuppEquiv Finset.sum Finset.univ instFintypeProd Pi.instFintype SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass Finsupp.instFunLike Finsupp.single Finset.prod CommSemiring.toCommMonoid	—	Finsupp.induction_linear RingHomInvPair.ids Finsupp.smulCommClass Algebra.to_smulCommClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finset.sum_congr zero_smul Finset.sum_const_zero map_add SemilinearMapClass.toAddHomClass Finsupp.smul_single add_mul Distrib.rightDistribClass Finsupp.single_add Finset.sum_add_distrib freeFinsuppEquiv_single Finsupp.single_apply ite_smul Finset.sum_ite_eq
freeFinsuppEquiv_def 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring MultilinearMap Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid instModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv freeFinsuppEquiv DFinsupp AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction LinearEquiv.multilinearMapCongrLeft finsuppLequivDFinsupp DFinsupp.smulCommClass LinearEquiv.symm LinearEquiv.multilinearMapCongrRight LinearMap.CompatibleSMul.finsupp_dom DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFinsupp.distribMulAction LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul DFinsupp.isScalarTower IsScalarTower.right LinearMap.CompatibleSMul.finsupp_cod LinearMap.IsScalarTower.compatibleSMul Algebra.toSMul freeDFinsuppEquiv Fintype.decidablePiFintype	—	RingHomInvPair.ids Finsupp.smulCommClass Algebra.to_smulCommClass
freeFinsuppEquiv_single 📖	mathematical	—	DFunLike.coe MultilinearMap Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule instFunLikeForall LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid instModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv freeFinsuppEquiv Finsupp.single SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass Finset.prod CommSemiring.toCommMonoid Finset.univ Finsupp.instFunLike	—	RingHomInvPair.ids Finsupp.smulCommClass Algebra.to_smulCommClass DFinsupp.smulCommClass LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' DFinsupp.isScalarTower IsScalarTower.right LinearMap.CompatibleSMul.finsupp_cod LinearMap.IsScalarTower.compatibleSMul smulCommClass_self Finsupp.toDFinsupp_single freeDFinsuppEquiv_single Finset.prod_congr map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass DFinsupp.toFinsupp_single Finsupp.smul_single

---

← Back to Index