Prod

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

Statistics

Metric	Count
Definitions instFintypeProd	1
Theorems product_eq_univ, univ_product_univ, card_prod, infinite_of_left, infinite_of_right, infinite_of_exists_right, infinite_of_left, infinite_of_right, toFinset_offDiag, toFinset_off_diag, toFinset_prod, infinite_prod	12
Total	13

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
product_eq_univ 📖	mathematical	—	SProd.sprod Finset instSProd univ instFintypeProd	—	—
univ_product_univ 📖	mathematical	—	SProd.sprod Finset instSProd univ instFintypeProd	—	—

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_prod 📖	mathematical	—	card instFintypeProd	—	Finset.card_product

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite_of_left 📖	mathematical	—	Infinite	—	Pi.infinite_of_left
infinite_of_right 📖	mathematical	—	Infinite	—	Pi.infinite_of_right

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite_of_exists_right 📖	mathematical	—	Infinite	—	Infinite.of_injective Function.update_injective
infinite_of_left 📖	mathematical	Nontrivial	Infinite	—	Infinite.of_injective of_not_not Function.update_of_ne exists_pair_ne
infinite_of_right 📖	—	Infinite	—	—	infinite_of_exists_right Nontrivial.to_nonempty Infinite.instNontrivial

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_offDiag 📖	mathematical	—	toFinset offDiag Finset.offDiag	—	Finset.ext
toFinset_off_diag 📖	mathematical	—	toFinset offDiag Finset.offDiag	—	toFinset_offDiag
toFinset_prod 📖	mathematical	—	toFinset SProd.sprod Set instSProd Finset Finset.instSProd	—	Finset.ext

(root)

Definitions

Name	Category	Theorems
instFintypeProd 📖	CompOp	91 math math: LinearMap.restrictScalars_toMatrix, Matrix.toLin_kronecker, Matrix.kroneckerTMulStarAlgEquiv_symm_apply, Matrix.compAlgEquiv_apply, SimpleGraph.two_mul_card_edgeFinset, Matrix.det_det, OrthonormalBasis.toBasis_tensorProduct, Matrix.trace_kronecker, AlternatingMap.domCoprod_coe, Equiv.Perm.OnCycleFactors.kerParam_range_card, Algebra.Norm.Transitivity.comp_det_mul_pow, TensorProduct.toMatrix_assoc, Matrix.toAlgEquiv_kroneckerStarAlgEquiv, Fintype.prod_prod_type_right, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Matrix.det_kroneckerMapBilinear, SimpleGraph.neighborFinset_completeEquipartiteGraph, Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv, Matrix.star_vec_dotProduct_vec, SimpleGraph.degree_completeEquipartiteGraph, Matrix.vec_dotProduct_vec, Fintype.prod_prod_type', Equiv.Perm.sign_prodExtendRight, OrthonormalBasis.tensorProduct_repr_tmul_apply', Matrix.kroneckerAlgEquiv_apply, Matrix.mul_kronecker_mul, Fintype.prod_prod_type, Finset.univ_product_univ, Matrix.det_kronecker, Finset.univ_perm_option, Matrix.IsUnit.kronecker, Matrix.compRingEquiv_symm_apply, Fintype.prod_prod_type_right', Matrix.kroneckerTMulAlgEquiv_symm_apply, Matrix.kroneckerTMulStarAlgEquiv_apply, evalRingHom_mapMatrix_comp_compRingEquiv, kroneckerTMulLinearEquiv_mul, Matrix.kronecker_mem_unitary, Fintype.card_prod, Algebra.smulTower_leftMulMatrix, OrthonormalBasis.tensorProduct_apply', NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, NumberField.mixedEmbedding.det_matrixToStdBasis, Finset.product_eq_univ, Algebra.Norm.Transitivity.eval_zero_comp_det, Matrix.vec_vecMul_kronecker_of_commute, Matrix.blockDiagonal_mul, Fintype.sum_prod_type', MultilinearMap.freeFinsuppEquiv_apply, Algebra.smulTower_leftMulMatrix_algebraMap_ne, Finset.univ_perm_fin_succ, Matrix.compAlgEquiv_symm_apply, Matrix.isUnit_comp_iff, Matrix.exp_blockDiagonal, Matrix.det_blockDiagonal, Matrix.inv_kronecker, Algebra.smulTower_leftMulMatrix_algebraMap, Matrix.vec_vecMul_kronecker, MultilinearMap.freeDFinsuppEquiv_apply, Matrix.kronecker_mulVec_vec, Matrix.kroneckerMapBilinear_mul_mul, Matrix.kroneckerAlgEquiv_symm_apply, Matrix.blockDiagonal_pow, Matrix.trace_kroneckerTMul, Matrix.mul_kroneckerTMul_mul, Matrix.kroneckerTMulAlgEquiv_apply, Matrix.trace_kroneckerMapBilinear, Matrix.trace_blockDiagonal, Matrix.toLinearEquiv_kroneckerAlgEquiv, Matrix.det_kroneckerTMul, Equiv.Perm.sign_prodCongrRight, SimpleGraph.card_edgeFinset_completeEquipartiteGraph, Matrix.compRingEquiv_apply, Matrix.blockDiagonalRingHom_apply, Fintype.sum_prod_type_right, Algebra.smulTower_leftMulMatrix_algebraMap_eq, Matrix.vec_mul_eq_vecMul, Equiv.Perm.sign_prodCongrLeft, OrthonormalBasis.tensorProduct_apply, Matrix.vec_mul_eq_mulVec, AlternatingMap.domCoprod_apply, matrixEquivTensor_apply, Fintype.sum_prod_type, Matrix.kronecker_mulVec_vec_of_commute, TensorProduct.toMatrix_comm, Matrix.kroneckerStarAlgEquiv_apply, TensorProduct.toMatrix_map, Fintype.sum_prod_type_right', OrthonormalBasis.tensorProduct_repr_tmul_apply, Matrix.kroneckerStarAlgEquiv_symm_apply, Matrix.isUnit_comp_symm_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite_prod 📖	mathematical	—	Infinite	—	Infinite.nonempty Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Finite.of_fintype Prod.infinite_of_left Prod.infinite_of_right

---

← Back to Index