Sigma

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

Statistics

Metric	Count
Definitions instFintype, instFintype	2
Theorems univ_sigma_univ, biInter_finsetSigma_univ, biInter_finsetSigma_univ', biUnion_finsetSigma_univ, biUnion_finsetSigma_univ'	5
Total	7

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
univ_sigma_univ 📖	mathematical	—	sigma univ Sigma.instFintype	—	—

PSigma

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter_finsetSigma_univ 📖	mathematical	—	iInter Finset Finset.instMembership Finset.sigma Finset.univ	—	iInter_congr_Prop ext
biInter_finsetSigma_univ' 📖	mathematical	—	iInter Finset Finset.instMembership Finset.sigma Finset.univ	—	iInter_congr_Prop ext
biUnion_finsetSigma_univ 📖	mathematical	—	iUnion Finset Finset.instMembership Finset.sigma Finset.univ	—	iUnion_congr_Prop ext
biUnion_finsetSigma_univ' 📖	mathematical	—	iUnion Finset Finset.instMembership Finset.sigma Finset.univ	—	iUnion_congr_Prop ext

Sigma

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	20 math math: Fintype.prod_sigma', Matrix.trace_blockDiagonal', Matrix.blockDiagonal'RingHom_apply, Fintype.prod_sigma, Pi.orthonormalBasis_apply, Fintype.card_sigma, LinearIsometryEquiv.piLpCurry_apply, Finset.univ_sigma_univ, Matrix.blockDiagonal'_mul, Pi.orthonormalBasis.toBasis, DirectSum.IsInternal.subordinateOrthonormalBasis_def, DirectSum.IsInternal.collectedOrthonormalBasis_mem, LinearIsometryEquiv.piLpCurry_symm_apply, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', Fintype.sum_sigma', Matrix.exp_blockDiagonal', LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, Fintype.sum_sigma, Pi.orthonormalBasis_repr, Matrix.blockDiagonal'_pow

---

← Back to Index