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 DFinsupp DFinsupp.addCommMonoid DFinsupp.module DFinsupp.distribMulAction DFinsupp.smulCommClass	—	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