DFinsupp

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

Statistics

Metric	Count
Definitions dfinsuppFamily, dfinsuppFamilyₗ, freeDFinsuppEquiv, fromDFinsuppEquiv	4
Theorems dfinsuppFamily_add, dfinsuppFamily_apply_support', dfinsuppFamily_apply_toFun, dfinsuppFamily_compLinearMap_lsingle, dfinsuppFamily_single, dfinsuppFamily_single_left, dfinsuppFamily_single_left_apply, dfinsuppFamily_smul, dfinsuppFamily_zero, dfinsuppFamilyₗ_apply, dfinsupp_ext, dfinsupp_ext_iff, freeDFinsuppEquiv_apply, freeDFinsuppEquiv_def, freeDFinsuppEquiv_single, fromDFinsuppEquiv_apply, fromDFinsuppEquiv_single, fromDFinsuppEquiv_symm_apply, support_dfinsuppFamily_subset	19
Total	23

MultilinearMap

Definitions

Name	Category	Theorems
dfinsuppFamily 📖	CompOp	11 math math: dfinsuppFamily_single, dfinsuppFamily_apply_toFun, dfinsuppFamily_apply_support', dfinsuppFamily_compLinearMap_lsingle, dfinsuppFamily_add, dfinsuppFamily_smul, dfinsuppFamilyₗ_apply, dfinsuppFamily_single_left_apply, support_dfinsuppFamily_subset, dfinsuppFamily_zero, dfinsuppFamily_single_left
dfinsuppFamilyₗ 📖	CompOp	1 math math: dfinsuppFamilyₗ_apply
freeDFinsuppEquiv 📖	CompOp	4 math math: freeDFinsuppEquiv_single, freeDFinsuppEquiv_def, freeFinsuppEquiv_def, freeDFinsuppEquiv_apply
fromDFinsuppEquiv 📖	CompOp	4 math math: fromDFinsuppEquiv_apply, fromDFinsuppEquiv_single, freeDFinsuppEquiv_def, fromDFinsuppEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dfinsuppFamily_add 📖	mathematical	—	dfinsuppFamily Pi.instAdd MultilinearMap instAdd DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	ext DFinsupp.ext
dfinsuppFamily_apply_support' 📖	mathematical	—	DFinsupp.support' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe MultilinearMap DFinsupp DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall dfinsuppFamily Trunc.map Multiset Multiset.map Finset.mem_univ Multiset.pi Finset.val Finset.univ Trunc.finChoice	—	—
dfinsuppFamily_apply_toFun 📖	mathematical	—	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike MultilinearMap DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall dfinsuppFamily	—	—
dfinsuppFamily_compLinearMap_lsingle 📖	mathematical	—	compLinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module dfinsuppFamily DFinsupp.lsingle LinearMap.compMultilinearMap Fintype.decidablePiFintype	—	ext dfinsuppFamily_single
dfinsuppFamily_single 📖	mathematical	—	DFunLike.coe MultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall dfinsuppFamily DFinsupp.single Fintype.decidablePiFintype	—	DFinsupp.ext eq_or_ne DFinsupp.single_apply DFinsupp.single_eq_of_ne Function.ne_iff map_coord_zero
dfinsuppFamily_single_left 📖	mathematical	—	dfinsuppFamily Pi.single MultilinearMap instZero Fintype.decidablePiFintype LinearMap.compMultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module DFinsupp.lsingle compLinearMap DFinsupp.lapply	—	ext dfinsuppFamily_single_left_apply
dfinsuppFamily_single_left_apply 📖	mathematical	—	DFunLike.coe MultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall dfinsuppFamily Pi.single instZero Fintype.decidablePiFintype DFinsupp.single DFinsupp.instDFunLike	—	DFinsupp.ext eq_or_ne Pi.single_eq_same DFinsupp.single_apply Pi.single_eq_of_ne'
dfinsuppFamily_smul 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	dfinsuppFamily Pi.instSMul MultilinearMap instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DFinsupp.addCommMonoid DFinsupp.module DFinsupp.instAddMonoid DFinsupp.distribMulAction DFinsupp.smulCommClass DistribSMul.toSMulZeroClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	ext DFinsupp.smulCommClass DFinsupp.ext
dfinsuppFamily_zero 📖	mathematical	—	dfinsuppFamily Pi.instZero MultilinearMap instZero DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module	—	ext DFinsupp.ext
dfinsuppFamilyₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module Pi.addCommMonoid addCommMonoid Pi.module instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFinsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul LinearMap.instFunLike dfinsuppFamilyₗ dfinsuppFamily	—	smulCommClass_self DFinsupp.smulCommClass
dfinsupp_ext 📖	—	compLinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module DFinsupp.lsingle	—	—	ext nonempty_fintype DFinsupp.sum_single map_sum_finset Finset.sum_congr
dfinsupp_ext_iff 📖	mathematical	—	compLinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module DFinsupp.lsingle	—	dfinsupp_ext
freeDFinsuppEquiv_apply 📖	mathematical	—	DFunLike.coe MultilinearMap DFinsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFinsupp.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFinsupp.module Semiring.toModule instFunLikeForall LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid instModule DFinsupp.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv freeDFinsuppEquiv Finset.sum Finset.univ instFintypeProd Pi.instFintype SMulZeroClass.toSMul DFinsupp.instZero DFinsupp.instSMulZeroClass DFinsupp.instDFunLike DFinsupp.single Finset.prod CommSemiring.toCommMonoid	—	DFinsupp.induction RingHomInvPair.ids DFinsupp.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 freeDFinsuppEquiv_single DFinsupp.single_apply add_smul ite_smul Finset.sum_add_distrib Finset.sum_ite_eq
freeDFinsuppEquiv_def 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids DFinsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring MultilinearMap DFinsupp.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFinsupp.module Semiring.toModule addCommMonoid instModule DFinsupp.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv freeDFinsuppEquiv AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid Pi.addCommMonoid Pi.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction fromDFinsuppEquiv LinearEquiv.piCongrRight piRingEquiv DFinsupp.linearEquivFunOnFintype Pi.instFintype DFinsupp.instZero DFinsupp.sigmaCurryLEquiv Fintype.decidablePiFintype DFinsupp.domLCongr Equiv.symm Equiv.sigmaEquivProd	—	RingHomInvPair.ids DFinsupp.smulCommClass Algebra.to_smulCommClass
freeDFinsuppEquiv_single 📖	mathematical	—	DFunLike.coe MultilinearMap DFinsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFinsupp.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFinsupp.module Semiring.toModule instFunLikeForall LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid instModule DFinsupp.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv freeDFinsuppEquiv DFinsupp.single Fintype.decidablePiFintype SMulZeroClass.toSMul DFinsupp.instZero DFinsupp.instSMulZeroClass Finset.prod CommSemiring.toCommMonoid Finset.univ DFinsupp.instDFunLike	—	RingHomInvPair.ids DFinsupp.smulCommClass Algebra.to_smulCommClass mul_one smul_eq_mul DFinsupp.single_smul map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass smul_apply DFinsupp.ext eq_or_ne Finset.prod_eq_zero Finset.mem_univ Equiv.right_inv smulCommClass_self mkPiRing_apply_one_eq_self fromDFinsuppEquiv_apply Finset.sum_congr DFinsupp.finset_sum_apply DFinsupp.single_apply mul_ite MulZeroClass.mul_zero Finset.sum_ite_eq Finset.prod_congr Finset.sum_const_zero
fromDFinsuppEquiv_apply 📖	mathematical	—	DFunLike.coe MultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid addCommMonoid Pi.module instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv fromDFinsuppEquiv Finset.sum Fintype.piFinset DFinsupp.support DFinsupp.instDFunLike	—	DFinsupp.sumAddHom_apply Finset.sum_subset support_dfinsuppFamily_subset
fromDFinsuppEquiv_single 📖	mathematical	—	DFunLike.coe MultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid addCommMonoid Pi.module instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv fromDFinsuppEquiv DFinsupp.single	—	RingHomInvPair.ids smulCommClass_self dfinsuppFamily_single DFinsupp.sumAddHom_single
fromDFinsuppEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids MultilinearMap DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module addCommMonoid Pi.addCommMonoid instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Pi.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm fromDFinsuppEquiv compLinearMap DFinsupp.lsingle	—	RingHomInvPair.ids smulCommClass_self
support_dfinsuppFamily_subset 📖	mathematical	—	Finset Finset.instHasSubset DFinsupp.support Fintype.decidablePiFintype AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe MultilinearMap DFinsupp DFinsupp.addCommMonoid DFinsupp.module instFunLikeForall dfinsuppFamily Fintype.piFinset	—	map_coord_zero

---

← Back to Index