Sum

📁 Source: Mathlib/Logic/Equiv/Sum.lean

Statistics

Metric	Count
Definitions `sumCongr`, `boolEquivPUnitSumPUnit`, `emptySum`, `prodSumDistrib`, `psumCongr`, `psumEquivSum`, `psumSum`, `sigmaEquivOptionOfInhabited`, `sigmaFiberEquiv`, `sigmaSumDistrib`, `subtypeSum`, `sumAssoc`, `sumComm`, `sumCompl`, `sumCongr`, `sumEmpty`, `sumEquivSigmaBool`, `sumPSum`, `sumSigmaDistrib`, `sumSumSumComm`, `Sum`	21
Theorems `sumCongr_apply`, `sumCongr_refl`, `sumCongr_symm`, `sumCongr_trans`, `emptySum_apply_inr`, `emptySum_symm_apply`, `prodSumDistrib_apply_left`, `prodSumDistrib_apply_right`, `prodSumDistrib_symm_apply_left`, `prodSumDistrib_symm_apply_right`, `sigmaFiberEquiv_apply`, `sigmaFiberEquiv_symm_apply_fst`, `sigmaFiberEquiv_symm_apply_snd_coe`, `sigmaSumDistrib_apply`, `sigmaSumDistrib_symm_apply`, `sumAssoc_apply_inl_inl`, `sumAssoc_apply_inl_inr`, `sumAssoc_apply_inr`, `sumAssoc_symm_apply_inl`, `sumAssoc_symm_apply_inr_inl`, `sumAssoc_symm_apply_inr_inr`, `sumComm_apply`, `sumComm_symm`, `sumCompl_apply_inl`, `sumCompl_apply_inr`, `sumCompl_apply_symm_of_neg`, `sumCompl_apply_symm_of_pos`, `sumCompl_symm_apply_neg`, `sumCompl_symm_apply_of_neg`, `sumCompl_symm_apply_of_pos`, `sumCompl_symm_apply_pos`, `sumCongr_apply`, `sumCongr_refl`, `sumCongr_symm`, `sumCongr_trans`, `sumEmpty_apply_inl`, `sumEmpty_symm_apply`, `sumSigmaDistrib_apply`, `sumSigmaDistrib_symm_apply`, `sumSumSumComm_apply`, `sumSumSumComm_symm`	41
Total	62

Equiv

Definitions

Name	Category	Theorems
`boolEquivPUnitSumPUnit` 📖	CompOp	—
`emptySum` 📖	CompOp	3 math math: `emptySum_apply_inr`, `emptySum_symm_apply`, `Homeomorph.coe_emptySum`
`prodSumDistrib` 📖	CompOp	5 math math: `prodSumDistrib_apply_left`, `prodSumDistrib_apply_right`, `prodSumDistrib_symm_apply_right`, `SimpleGraph.Iso.boxProdSumDistrib_toEquiv`, `prodSumDistrib_symm_apply_left`
`psumCongr` 📖	CompOp	—
`psumEquivSum` 📖	CompOp	—
`psumSum` 📖	CompOp	—
`sigmaEquivOptionOfInhabited` 📖	CompOp	—
`sigmaFiberEquiv` 📖	CompOp	8 math math: `sigmaFiberEquiv_apply`, `ofFiberEquiv_apply`, `ofPreimageEquiv_apply`, `sigmaFiberEquiv_symm_apply_fst`, `sigmaFiberEquiv_symm_apply_snd_coe`, `ofFiberEquiv_symm_apply`, `ofPreimageEquiv_symm_apply`, `DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe`
`sigmaSumDistrib` 📖	CompOp	2 math math: `sigmaSumDistrib_symm_apply`, `sigmaSumDistrib_apply`
`subtypeSum` 📖	CompOp	—
`sumAssoc` 📖	CompOp	14 math math: `sumAssoc_symm_apply_inl`, `sumAssoc_apply_inr`, `FirstOrder.Language.Term.constantsVarsEquivLeft_apply`, `LieAlgebra.Orthogonal.indefiniteDiagonal_assoc`, `sumAssoc_apply_inl_inl`, `Diffeomorph.sumAssoc_coe`, `sumAssoc_apply_inl_inr`, `Homeomorph.continuous_sumAssoc`, `FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply`, `Homeomorph.continuous_sumAssoc_symm`, `sumAssoc_symm_apply_inr_inl`, `sumSumSumComm_apply`, `sumAssoc_symm_apply_inr_inr`, `Homeomorph.sumAssoc_toEquiv`
`sumComm` 📖	CompOp	6 math math: `Finset.toLeft_map_sumComm`, `Polynomial.sylvester_comm`, `sumComm_symm`, `Finset.toRight_map_sumComm`, `sumSumSumComm_apply`, `sumComm_apply`
`sumCompl` 📖	CompOp	12 math math: `sumCompl_symm_apply_pos`, `RelIso.sumLexComplRight_apply`, `RelIso.sumLexComplLeft_symm_apply`, `sumCompl_apply_inl`, `sumCompl_apply_inr`, `sumCompl_apply_symm_of_neg`, `RelIso.sumLexComplRight_symm_apply`, `sumCompl_apply_symm_of_pos`, `sumCompl_symm_apply_neg`, `RelIso.sumLexComplLeft_apply`, `sumCompl_symm_apply_of_neg`, `sumCompl_symm_apply_of_pos`
`sumCongr` 📖	CompOp	5 math math: `sumCongr_refl`, `MultilinearMap.domCoprod_domDomCongr_sumCongr`, `sumCongr_trans`, `sumCongr_apply`, `sumCongr_symm`
`sumEmpty` 📖	CompOp	4 math math: `sumEmpty_symm_apply`, `RelIso.emptySumLex_apply`, `Diffeomorph.sumEmpty_toEquiv`, `sumEmpty_apply_inl`
`sumEquivSigmaBool` 📖	CompOp	—
`sumPSum` 📖	CompOp	—
`sumSigmaDistrib` 📖	CompOp	2 math math: `sumSigmaDistrib_symm_apply`, `sumSigmaDistrib_apply`
`sumSumSumComm` 📖	CompOp	3 math math: `Homeomorph.sumSumSumComm_toEquiv`, `sumSumSumComm_symm`, `sumSumSumComm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`emptySum_apply_inr` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `emptySum`	—	—
`emptySum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `emptySum`	—	—
`prodSumDistrib_apply_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `prodSumDistrib`	—	—
`prodSumDistrib_apply_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `prodSumDistrib`	—	—
`prodSumDistrib_symm_apply_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `prodSumDistrib`	—	—
`prodSumDistrib_symm_apply_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `prodSumDistrib`	—	—
`sigmaFiberEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sigmaFiberEquiv`	—	—
`sigmaFiberEquiv_symm_apply_fst` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sigmaFiberEquiv`	—	—
`sigmaFiberEquiv_symm_apply_snd_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sigmaFiberEquiv`	—	—
`sigmaSumDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sigmaSumDistrib`	—	—
`sigmaSumDistrib_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sigmaSumDistrib` `Sigma.map`	—	—
`sumAssoc_apply_inl_inl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumAssoc`	—	—
`sumAssoc_apply_inl_inr` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumAssoc`	—	—
`sumAssoc_apply_inr` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumAssoc`	—	—
`sumAssoc_symm_apply_inl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumAssoc`	—	—
`sumAssoc_symm_apply_inr_inl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumAssoc`	—	—
`sumAssoc_symm_apply_inr_inr` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumAssoc`	—	—
`sumComm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumComm`	—	—
`sumComm_symm` 📖	mathematical	—	`symm` `sumComm`	—	—
`sumCompl_apply_inl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumCompl`	—	—
`sumCompl_apply_inr` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumCompl`	—	—
`sumCompl_apply_symm_of_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumCompl`	—	`sumCompl_symm_apply_of_neg`
`sumCompl_apply_symm_of_pos` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumCompl`	—	`sumCompl_symm_apply_of_pos`
`sumCompl_symm_apply_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumCompl`	—	`sumCompl_symm_apply_of_neg`
`sumCompl_symm_apply_of_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumCompl`	—	—
`sumCompl_symm_apply_of_pos` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumCompl`	—	—
`sumCompl_symm_apply_pos` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumCompl`	—	`sumCompl_symm_apply_of_pos`
`sumCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumCongr`	—	—
`sumCongr_refl` 📖	mathematical	—	`sumCongr` `refl`	—	`Perm.ext`
`sumCongr_symm` 📖	mathematical	—	`symm` `sumCongr`	—	—
`sumCongr_trans` 📖	mathematical	—	`trans` `sumCongr`	—	`ext`
`sumEmpty_apply_inl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumEmpty`	—	—
`sumEmpty_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumEmpty`	—	—
`sumSigmaDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumSigmaDistrib`	—	—
`sumSigmaDistrib_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `sumSigmaDistrib`	—	—
`sumSumSumComm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `sumSumSumComm` `sumAssoc` `symm` `sumComm`	—	—
`sumSumSumComm_symm` 📖	mathematical	—	`symm` `sumSumSumComm`	—	—

Equiv.Perm

Definitions

Name	Category	Theorems
`sumCongr` 📖	CompOp	13 math math: `sumCongr_swap_refl`, `sumCongr_symm`, `sumCongr_inv`, `sumCongr_refl`, `sumCongr_apply`, `sumCongr_trans`, `sign_sumCongr`, `sumCongr_swap_one`, `sumCongr_one_swap`, `sumCongr_one`, `sumCongr_mul`, `sumCongr_refl_swap`, `sumCongrHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sumCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `sumCongr`	—	—
`sumCongr_refl` 📖	mathematical	—	`sumCongr` `Equiv.refl`	—	`Equiv.sumCongr_refl`
`sumCongr_symm` 📖	mathematical	—	`Equiv.symm` `sumCongr`	—	`Equiv.sumCongr_symm`
`sumCongr_trans` 📖	mathematical	—	`Equiv.trans` `sumCongr`	—	`Equiv.sumCongr_trans`

Mathlib.Tactic.Linarith

Definitions

Name	Category	Theorems
`Sum` 📖	CompOp	—

---

← Back to Index