Documentation Verification Report

Sigma

📁 Source: Mathlib/Data/DFinsupp/Sigma.lean

Statistics

Metric	Count
Definitions `sigmaCurry`, `sigmaCurryEquiv`, `sigmaUncurry`	3
Theorems `sigmaCurry_add`, `sigmaCurry_apply`, `sigmaCurry_single`, `sigmaCurry_smul`, `sigmaCurry_zero`, `sigmaUncurry_add`, `sigmaUncurry_apply`, `sigmaUncurry_single`, `sigmaUncurry_smul`, `sigmaUncurry_zero`	10
Total	13

DFinsupp

Definitions

Name	Category	Theorems
`sigmaCurry` 📖	CompOp	5 math math: `sigmaCurry_single`, `sigmaCurry_smul`, `sigmaCurry_zero`, `sigmaCurry_add`, `sigmaCurry_apply`
`sigmaCurryEquiv` 📖	CompOp	2 math math: `sigmaCurryLEquiv_apply`, `sigmaCurryLEquiv_symm_apply`
`sigmaUncurry` 📖	CompOp	5 math math: `sigmaUncurry_add`, `sigmaUncurry_single`, `sigmaUncurry_apply`, `sigmaUncurry_smul`, `sigmaUncurry_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigmaCurry_add` 📖	mathematical	—	`sigmaCurry` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp` `instAdd` `instZero` `hasAdd₂`	—	`ext`
`sigmaCurry_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `instDFunLike` `instZero` `sigmaCurry`	—	—
`sigmaCurry_single` 📖	mathematical	—	`sigmaCurry` `single` `Sigma.instDecidableEqSigma` `DFinsupp` `instZero`	—	`ext` `sigmaCurry_apply` `eq_or_ne` `single_eq_same` `single_eq_of_ne` `single_apply`
`sigmaCurry_smul` 📖	mathematical	—	`sigmaCurry` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`ext`
`sigmaCurry_zero` 📖	mathematical	—	`sigmaCurry` `DFinsupp` `instZero`	—	—
`sigmaUncurry_add` 📖	mathematical	—	`sigmaUncurry` `AddZero.toZero` `AddZeroClass.toAddZero` `DFinsupp` `instZero` `hasAdd₂` `instAdd`	—	`DFunLike.coe_injective`
`sigmaUncurry_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `instDFunLike` `sigmaUncurry` `instZero`	—	—
`sigmaUncurry_single` 📖	mathematical	—	`sigmaUncurry` `single` `DFinsupp` `instZero` `Sigma.instDecidableEqSigma`	—	`ext` `sigmaUncurry_apply` `eq_or_ne` `single_eq_same` `single_eq_of_ne` `single_apply`
`sigmaUncurry_smul` 📖	mathematical	—	`sigmaUncurry` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFinsupp` `instZero` `SMulZeroClass.toSMul` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`DFunLike.coe_injective`
`sigmaUncurry_zero` 📖	mathematical	—	`sigmaUncurry` `DFinsupp` `instZero`	—	—

---

← Back to Index