Pi

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

Statistics

Metric	Count
Definitions piFinset, fintype, instFintype, instFintype, instFintype	5
Theorems piFinset_const, piDiag_subset_piFinset, piFinset_filter_const, univ_pi_univ, piFinset_nonempty_of_forall_nonempty, coe_piFinset, eval_image_piFinset, eval_image_piFinset_const, eval_image_piFinset_subset, filter_piFinset_of_notMem, mem_piFinset, piFinset_disjoint_of_disjoint, piFinset_empty, piFinset_eq_empty, piFinset_image, piFinset_nonempty, piFinset_of_isEmpty, piFinset_singleton, piFinset_subset, piFinset_subsingleton, piFinset_univ, piFinset_update_eq_filter_piFinset_mem, piFinset_update_singleton_eq_filter_piFinset_eq, pi, pi', forall_finite_image_eval_iff	26
Total	31

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piDiag_subset_piFinset 📖	mathematical	—	Finset instHasSubset piDiag Fintype.piFinset	—	—
piFinset_filter_const 📖	mathematical	—	filter Finset instMembership decidableExistsAndFinset Fintype.piFinset piDiag	—	ext
univ_pi_univ 📖	mathematical	—	pi univ Pi.instFintype pfunFintype Finset instMembership decidableMem	—	ext

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piFinset_const 📖	mathematical	Finset.Nonempty	Fintype.piFinset	—	Fintype.piFinset_nonempty

Fintype

Definitions

Name	Category	Theorems
piFinset 📖	CompOp	75 math math: piFinset_vadd_finset, mem_piFinset, MultilinearMap.fromDFinsuppEquiv_apply, piFinset_image, Aesop.piFinset_nonempty_of_forall_nonempty, piFinset_univ, Finset.card_insertNthEquiv_filter_piFinset, Fin.mem_piFinset_iff_pivot_removeNth, piFinset_vadd, filter_piFinset_of_notMem, Finset.map_consEquiv_filter_piFinset, MvPolynomial.schwartz_zippel_totalDegree, card_filter_piFinset_eq, Finset.map_snocEquiv_filter_piFinset, Finset.card_snocEquiv_filter_piFinset, card_piFinset_const, piFinset_update_eq_filter_piFinset_mem, Fin.insertNth_mem_piFinset_insertNth, sum_piFinset_apply, Finset.Nonempty.piFinset_const, piFinset_add, piFinset_neg, piFinset_update_singleton_eq_filter_piFinset_eq, Finset.prod_univ_pi, card_piFinset, ContinuousAlternatingMap.map_sum_finset, piFinset_subset, Finset.filter_piFinset_eq_map_consEquiv, piFinset_empty, Finset.filter_piFinset_eq_map_insertNthEquiv, Finset.piDiag_subset_piFinset, MultilinearMap.map_sum_finset_aux, Fin.snoc_mem_piFinset_snoc, Pi.uIcc_eq, Finset.card_consEquiv_filter_piFinset, piFinset_sub, card_filter_piFinset_eq_of_mem, MvPolynomial.schwartz_zippel_sup_sum, card_filter_piFinset_const_eq_of_mem, piFinset_of_isEmpty, coe_piFinset, eval_image_piFinset_subset, MultilinearMap.fromDirectSumEquiv_apply, piFinset_eq_empty, piFinset_smul, piFinset_mul, piFinset_disjoint_of_disjoint, piFinset_image₂, Finset.piFinset_filter_const, Finset.map_insertNthEquiv_filter_piFinset, piFinset_smul_finset, Finset.filter_piFinset_eq_map_snocEquiv, piFinset_inv, MultilinearMap.support_dfinsuppFamily_subset, piFinset_div, Fin.cons_mem_piFinset_cons, MultilinearMap.map_sum_finset, Fin.mem_piFinset_iff_last_init, piFinset_singleton, ContinuousMultilinearMap.map_sum_finset, Finset.sum_univ_pi, card_filter_piFinset_const, eval_image_piFinset_const, Fin.mem_piFinset_iff_zero_tail, MvPolynomial.schwartz_zippel_sum_degreeOf, piFinset_subsingleton, Finset.prod_univ_sum, ZLattice.sum_piFinset_Icc_rpow_le, Finset.sum_prod_piFinset, Finset.expect_pow, piFinset_nonempty, eval_image_piFinset, Finset.sum_pow', Nat.finMulAntidiag_eq_piFinset_divisors_filter, Pi.Icc_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_piFinset 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike piFinset Set.pi Set.univ	—	Set.ext Set.mem_univ_pi mem_piFinset
eval_image_piFinset 📖	mathematical	Finset.Nonempty	Finset.image piFinset	—	HasSubset.Subset.antisymm Finset.instAntisymmSubset eval_image_piFinset_subset Finset.mem_image
eval_image_piFinset_const 📖	mathematical	—	Finset.image piFinset	—	Finset.eq_empty_or_nonempty piFinset_empty eval_image_piFinset
eval_image_piFinset_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.image piFinset	—	Finset.image_subset_iff mem_piFinset
filter_piFinset_of_notMem 📖	mathematical	Finset Finset.instMembership	Finset.filter piFinset Finset.instEmptyCollection	—	—
mem_piFinset 📖	mathematical	—	Finset Finset.instMembership piFinset	—	Finset.mem_univ
piFinset_disjoint_of_disjoint 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	piFinset	—	Finset.disjoint_iff_ne mem_piFinset
piFinset_empty 📖	mathematical	—	piFinset Finset Finset.instEmptyCollection	—	—
piFinset_eq_empty 📖	mathematical	—	piFinset Finset Finset.instEmptyCollection	—	Finset.mem_univ
piFinset_image 📖	mathematical	—	piFinset Finset.image decidablePiFintype	—	Finset.ext
piFinset_nonempty 📖	mathematical	—	Finset.Nonempty piFinset	—	Finset.mem_univ
piFinset_of_isEmpty 📖	mathematical	—	piFinset Finset.univ Unique.fintype Pi.uniqueOfIsEmpty	—	Finset.eq_univ_of_forall
piFinset_singleton 📖	mathematical	—	piFinset Finset Finset.instSingleton	—	Finset.ext
piFinset_subset 📖	mathematical	Finset Finset.instHasSubset	piFinset	—	mem_piFinset
piFinset_subsingleton 📖	mathematical	Set.Subsingleton SetLike.coe Finset Finset.instSetLike	piFinset	—	mem_piFinset
piFinset_univ 📖	mathematical	—	piFinset Finset.univ Pi.instFintype	—	—
piFinset_update_eq_filter_piFinset_mem 📖	mathematical	Finset Finset.instHasSubset	piFinset Function.update Finset.filter Finset.instMembership Finset.decidableMem	—	—
piFinset_update_singleton_eq_filter_piFinset_eq 📖	mathematical	Finset Finset.instMembership	piFinset Function.update Finset.instSingleton Finset.filter	—	—

Fintype.Aesop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piFinset_nonempty_of_forall_nonempty 📖	mathematical	Finset.Nonempty	Fintype.piFinset	—	Fintype.piFinset_nonempty

Function.Embedding

Definitions

Name	Category	Theorems
fintype 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	22 math math: Fintype.card_pi, Finset.univ_pi_univ, Fintype.piFinset_univ, Equiv.Perm.OnCycleFactors.kerParam_range_card, char_dvd_card_solutions_of_add_lt, MultilinearMap.map_sum, ContinuousMultilinearMap.map_sum, MvPolynomial.rank_R, Fintype.sum_pow, Fintype.card_pi_const, ContinuousAlternatingMap.map_sum, Fintype.prod_sum, MvPolynomial.finrank_R, MultilinearMap.freeDFinsuppEquiv_def, PiTensorProduct.dualDistribInvOfBasis_apply, MultilinearMap.freeFinsuppEquiv_apply, char_dvd_card_solutions, char_dvd_card_solutions_of_sum_lt, MultilinearMap.freeDFinsuppEquiv_apply, MvPolynomial.sum_eval_eq_zero, Fintype.card_fun, char_dvd_card_solutions_of_fintype_sum_lt

RelEmbedding

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	—

RelHom

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_finite_image_eval_iff 📖	mathematical	—	Finite image Function.eval	—	Finite.subset Finite.pi subset_pi_eval_image Finite.image

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	Set.Finite	Set.pi Set.univ	—	nonempty_fintype CanLift.prf Pi.canLift Set.instCanLiftFinsetCoeFinite Fintype.coe_piFinset Finset.finite_toSet
pi' 📖	mathematical	Set.Finite	setOf	—	pi

---

← Back to Index