Documentation Verification Report

SumProd

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

Statistics

Metric	Count
Definitions `sigmaFinsuppLEquivPiFinsupp`, `sumFinsuppLEquivProdFinsupp`	2
Theorems `fst_sumFinsuppLEquivProdFinsupp`, `sigmaFinsuppLEquivPiFinsupp_apply`, `sigmaFinsuppLEquivPiFinsupp_symm_apply`, `snd_sumFinsuppLEquivProdFinsupp`, `sumFinsuppLEquivProdFinsupp_apply`, `sumFinsuppLEquivProdFinsupp_symm_apply`, `sumFinsuppLEquivProdFinsupp_symm_inl`, `sumFinsuppLEquivProdFinsupp_symm_inr`	8
Total	10

Finsupp

Definitions

Name	Category	Theorems
`sigmaFinsuppLEquivPiFinsupp` 📖	CompOp	2 math math: `sigmaFinsuppLEquivPiFinsupp_symm_apply`, `sigmaFinsuppLEquivPiFinsupp_apply`
`sumFinsuppLEquivProdFinsupp` 📖	CompOp	6 math math: `snd_sumFinsuppLEquivProdFinsupp`, `fst_sumFinsuppLEquivProdFinsupp`, `sumFinsuppLEquivProdFinsupp_apply`, `sumFinsuppLEquivProdFinsupp_symm_apply`, `sumFinsuppLEquivProdFinsupp_symm_inl`, `sumFinsuppLEquivProdFinsupp_symm_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_sumFinsuppLEquivProdFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `Prod.instAddCommMonoid` `module` `Prod.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `sumFinsuppLEquivProdFinsupp`	—	`RingHomInvPair.ids`
`sigmaFinsuppLEquivPiFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `Pi.addCommMonoid` `module` `Pi.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `sigmaFinsuppLEquivPiFinsupp`	—	`RingHomInvPair.ids`
`sigmaFinsuppLEquivPiFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `instAddCommMonoid` `Pi.module` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `sigmaFinsuppLEquivPiFinsupp`	—	`RingHomInvPair.ids`
`snd_sumFinsuppLEquivProdFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `instAddCommMonoid` `Prod.instAddCommMonoid` `module` `Prod.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `sumFinsuppLEquivProdFinsupp`	—	`RingHomInvPair.ids`
`sumFinsuppLEquivProdFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Prod.instAddCommMonoid` `module` `Prod.instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `sumFinsuppLEquivProdFinsupp` `Equiv.toFun` `AddEquiv.toEquiv` `instAdd` `Prod.instAdd` `sumFinsuppAddEquivProdFinsupp`	—	`RingHomInvPair.ids`
`sumFinsuppLEquivProdFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Prod.instAddCommMonoid` `instAddCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `sumFinsuppLEquivProdFinsupp` `Equiv.invFun` `AddEquiv.toEquiv` `instAdd` `Prod.instAdd` `sumFinsuppAddEquivProdFinsupp`	—	`RingHomInvPair.ids`
`sumFinsuppLEquivProdFinsupp_symm_inl` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `instAddCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `sumFinsuppLEquivProdFinsupp`	—	`RingHomInvPair.ids`
`sumFinsuppLEquivProdFinsupp_symm_inr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `instAddCommMonoid` `Prod.instModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `sumFinsuppLEquivProdFinsupp`	—	`RingHomInvPair.ids`

---

← Back to Index