Documentation Verification Report

ToDFinsupp

📁 Source: Mathlib/Data/Finsupp/ToDFinsupp.lean

Statistics

Metric	Count
Definitions `toFinsupp`, `toDFinsupp`, `finsuppAddEquivDFinsupp`, `finsuppEquivDFinsupp`, `finsuppLequivDFinsupp`, `sigmaFinsuppAddEquivDFinsupp`, `sigmaFinsuppEquivDFinsupp`, `sigmaFinsuppLequivDFinsupp`	8
Theorems `toFinsupp_add`, `toFinsupp_coe`, `toFinsupp_neg`, `toFinsupp_single`, `toFinsupp_smul`, `toFinsupp_sub`, `toFinsupp_support`, `toFinsupp_toDFinsupp`, `toFinsupp_zero`, `toDFinsupp_add`, `toDFinsupp_coe`, `toDFinsupp_neg`, `toDFinsupp_single`, `toDFinsupp_smul`, `toDFinsupp_sub`, `toDFinsupp_toFinsupp`, `toDFinsupp_zero`, `finsuppAddEquivDFinsupp_apply`, `finsuppAddEquivDFinsupp_symm_apply`, `finsuppEquivDFinsupp_apply`, `finsuppEquivDFinsupp_symm_apply`, `finsuppLequivDFinsupp_apply_apply`, `finsuppLequivDFinsupp_symm_apply`, `sigmaFinsuppAddEquivDFinsupp_apply`, `sigmaFinsuppAddEquivDFinsupp_symm_apply`, `sigmaFinsuppEquivDFinsupp_add`, `sigmaFinsuppEquivDFinsupp_apply`, `sigmaFinsuppEquivDFinsupp_single`, `sigmaFinsuppEquivDFinsupp_smul`, `sigmaFinsuppEquivDFinsupp_support`, `sigmaFinsuppEquivDFinsupp_symm_apply`, `sigmaFinsuppLequivDFinsupp_apply`, `sigmaFinsuppLequivDFinsupp_symm_apply`, `toDFinsupp_support`	34
Total	42

DFinsupp

Definitions

Name	Category	Theorems
`toFinsupp` 📖	CompOp	13 math math: `toFinsupp_add`, `toFinsupp_sub`, `toFinsupp_smul`, `toFinsupp_toDFinsupp`, `toFinsupp_coe`, `toFinsupp_single`, `Finsupp.toDFinsupp_toFinsupp`, `toFinsupp_support`, `finsuppEquivDFinsupp_symm_apply`, `finsuppLequivDFinsupp_symm_apply`, `finsuppAddEquivDFinsupp_symm_apply`, `toFinsupp_neg`, `toFinsupp_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFinsupp_add` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp` `instAdd` `Finsupp` `Finsupp.instAdd`	—	`DFunLike.coe_injective` `coe_add`
`toFinsupp_coe` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `toFinsupp` `DFinsupp` `instDFunLike`	—	—
`toFinsupp_neg` 📖	mathematical	—	`toFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DFinsupp` `instNeg` `Finsupp` `Finsupp.instNeg`	—	`DFunLike.coe_injective` `coe_neg`
`toFinsupp_single` 📖	mathematical	—	`toFinsupp` `single` `Finsupp.single`	—	`Finsupp.ext` `single_apply` `Finsupp.single_apply`
`toFinsupp_smul` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Finsupp` `Finsupp.instZero` `Finsupp.smulZeroClass`	—	`DFunLike.coe_injective` `coe_smul`
`toFinsupp_sub` 📖	mathematical	—	`toFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DFinsupp` `instSub` `Finsupp` `Finsupp.instSub`	—	`DFunLike.coe_injective` `coe_sub`
`toFinsupp_support` 📖	mathematical	—	`Finsupp.support` `toFinsupp` `support`	—	`Finset.ext`
`toFinsupp_toDFinsupp` 📖	mathematical	—	`Finsupp.toDFinsupp` `toFinsupp`	—	`DFunLike.coe_injective`
`toFinsupp_zero` 📖	mathematical	—	`toFinsupp` `DFinsupp` `instZero` `Finsupp` `Finsupp.instZero`	—	`DFunLike.coe_injective`

Finsupp

Definitions

Name	Category	Theorems
`toDFinsupp` 📖	CompOp	14 math math: `toDFinsupp_add`, `toDFinsupp_support`, `DFinsupp.toFinsupp_toDFinsupp`, `toDFinsupp_coe`, `finsuppEquivDFinsupp_apply`, `toDFinsupp_toFinsupp`, `toDFinsupp_smul`, `toDFinsupp_neg`, `toDFinsupp_sub`, `lex_eq_invImage_dfinsupp_lex`, `finsuppLequivDFinsupp_apply_apply`, `finsuppAddEquivDFinsupp_apply`, `toDFinsupp_zero`, `toDFinsupp_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toDFinsupp_add` 📖	mathematical	—	`toDFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `instAdd` `DFinsupp` `DFinsupp.instAdd`	—	`DFunLike.coe_injective`
`toDFinsupp_coe` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `DFinsupp.instDFunLike` `toDFinsupp` `Finsupp` `instFunLike`	—	—
`toDFinsupp_neg` 📖	mathematical	—	`toDFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `instNeg` `DFinsupp` `DFinsupp.instNeg`	—	`DFunLike.coe_injective`
`toDFinsupp_single` 📖	mathematical	—	`toDFinsupp` `single` `DFinsupp.single`	—	`DFinsupp.ext` `single_apply` `DFinsupp.single_apply`
`toDFinsupp_smul` 📖	mathematical	—	`toDFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DFinsupp` `DFinsupp.instZero` `DFinsupp.instSMulZeroClass`	—	`DFunLike.coe_injective`
`toDFinsupp_sub` 📖	mathematical	—	`toDFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `instSub` `DFinsupp` `DFinsupp.instSub`	—	`DFunLike.coe_injective`
`toDFinsupp_toFinsupp` 📖	mathematical	—	`DFinsupp.toFinsupp` `toDFinsupp`	—	`DFunLike.coe_injective`
`toDFinsupp_zero` 📖	mathematical	—	`toDFinsupp` `Finsupp` `instZero` `DFinsupp` `DFinsupp.instZero`	—	`DFunLike.coe_injective`

(root)

Definitions

Name	Category	Theorems
`finsuppAddEquivDFinsupp` 📖	CompOp	2 math math: `finsuppAddEquivDFinsupp_apply`, `finsuppAddEquivDFinsupp_symm_apply`
`finsuppEquivDFinsupp` 📖	CompOp	2 math math: `finsuppEquivDFinsupp_apply`, `finsuppEquivDFinsupp_symm_apply`
`finsuppLequivDFinsupp` 📖	CompOp	4 math math: `MultilinearMap.freeFinsuppEquiv_def`, `finsuppLequivDFinsupp_apply_apply`, `finsuppLequivDFinsupp_symm_apply`, `lsum_comp_mapRange_toSpanSingleton`
`sigmaFinsuppAddEquivDFinsupp` 📖	CompOp	4 math math: `sigmaFinsuppAddEquivDFinsupp_apply`, `sigmaFinsuppAddEquivDFinsupp_symm_apply`, `sigmaFinsuppLequivDFinsupp_symm_apply`, `sigmaFinsuppLequivDFinsupp_apply`
`sigmaFinsuppEquivDFinsupp` 📖	CompOp	8 math math: `sigmaFinsuppEquivDFinsupp_support`, `sigmaFinsuppAddEquivDFinsupp_apply`, `sigmaFinsuppAddEquivDFinsupp_symm_apply`, `sigmaFinsuppEquivDFinsupp_add`, `sigmaFinsuppEquivDFinsupp_symm_apply`, `sigmaFinsuppEquivDFinsupp_smul`, `sigmaFinsuppEquivDFinsupp_single`, `sigmaFinsuppEquivDFinsupp_apply`
`sigmaFinsuppLequivDFinsupp` 📖	CompOp	2 math math: `sigmaFinsuppLequivDFinsupp_symm_apply`, `sigmaFinsuppLequivDFinsupp_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsuppAddEquivDFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp` `Finsupp.instAdd` `DFinsupp.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `finsuppAddEquivDFinsupp` `Finsupp.toDFinsupp`	—	—
`finsuppAddEquivDFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `DFinsupp.instAdd` `Finsupp.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `finsuppAddEquivDFinsupp` `DFinsupp.toFinsupp`	—	—
`finsuppEquivDFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `DFinsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppEquivDFinsupp` `Finsupp.toDFinsupp`	—	—
`finsuppEquivDFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DFinsupp` `Finsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finsuppEquivDFinsupp` `DFinsupp.toFinsupp`	—	—
`finsuppLequivDFinsupp_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp` `Finsupp.instAddCommMonoid` `DFinsupp.addCommMonoid` `Finsupp.module` `DFinsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `finsuppLequivDFinsupp` `Finsupp.toDFinsupp`	—	`RingHomInvPair.ids`
`finsuppLequivDFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp` `DFinsupp.addCommMonoid` `Finsupp.instAddCommMonoid` `DFinsupp.module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `finsuppLequivDFinsupp` `DFinsupp.toFinsupp`	—	`RingHomInvPair.ids`
`sigmaFinsuppAddEquivDFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp` `Finsupp.instAddZeroClass` `Finsupp.instAdd` `DFinsupp.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `sigmaFinsuppAddEquivDFinsupp` `Equiv` `Finsupp.instZero` `Equiv.instEquivLike` `sigmaFinsuppEquivDFinsupp`	—	—
`sigmaFinsuppAddEquivDFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `DFinsupp` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `DFinsupp.instAdd` `Finsupp.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `sigmaFinsuppAddEquivDFinsupp` `Equiv` `Finsupp.instZero` `Equiv.instEquivLike` `Equiv.symm` `sigmaFinsuppEquivDFinsupp`	—	—
`sigmaFinsuppEquivDFinsupp_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp` `Finsupp.instZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaFinsuppEquivDFinsupp` `Finsupp.instAdd` `DFinsupp.instAdd` `Finsupp.instAddZeroClass`	—	`DFinsupp.ext` `Finsupp.ext`
`sigmaFinsuppEquivDFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `Finsupp` `Finsupp.instZero` `DFinsupp.instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaFinsuppEquivDFinsupp` `Finsupp.split`	—	—
`sigmaFinsuppEquivDFinsupp_single` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `DFinsupp` `Finsupp.instZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaFinsuppEquivDFinsupp` `Finsupp.single` `DFinsupp.single`	—	`DFinsupp.ext` `Finsupp.ext` `Finsupp.split_apply` `Finsupp.single_apply` `DFinsupp.single_apply`
`sigmaFinsuppEquivDFinsupp_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFinsupp` `Finsupp.instZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaFinsuppEquivDFinsupp` `SMulZeroClass.toSMul` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DFinsupp.instZero` `DFinsupp.instSMulZeroClass`	—	`DFinsupp.ext` `Finsupp.ext`
`sigmaFinsuppEquivDFinsupp_support` 📖	mathematical	—	`DFinsupp.support` `Finsupp` `Finsupp.instZero` `DFunLike.coe` `Equiv` `DFinsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaFinsuppEquivDFinsupp` `Finsupp.splitSupport`	—	`Finset.ext` `DFinsupp.mem_support_toFun` `Finsupp.mem_splitSupport_iff_nonzero`
`sigmaFinsuppEquivDFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `Equiv` `DFinsupp` `Finsupp.instZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sigmaFinsuppEquivDFinsupp` `DFinsupp.instDFunLike`	—	—
`sigmaFinsuppLequivDFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp` `Finsupp.instAddCommMonoid` `DFinsupp.addCommMonoid` `Finsupp.module` `DFinsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `sigmaFinsuppLequivDFinsupp` `Equiv.toFun` `Finsupp.instAddZeroClass` `AddEquiv.toEquiv` `Finsupp.instAdd` `DFinsupp.instAdd` `sigmaFinsuppAddEquivDFinsupp`	—	`RingHomInvPair.ids`
`sigmaFinsuppLequivDFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DFinsupp` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `DFinsupp.addCommMonoid` `DFinsupp.module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `sigmaFinsuppLequivDFinsupp` `Equiv.invFun` `Finsupp.instAddZeroClass` `AddEquiv.toEquiv` `Finsupp.instAdd` `DFinsupp.instAdd` `sigmaFinsuppAddEquivDFinsupp`	—	`RingHomInvPair.ids`
`toDFinsupp_support` 📖	mathematical	—	`DFinsupp.support` `Finsupp.toDFinsupp` `Finsupp.support`	—	`Finset.ext`

---

← Back to Index