Pi

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

Statistics

Metric	Count
Definitions cons, empty, pi	3
Theorems pi, cons_eta, cons_injective, cons_map, cons_ne, cons_same, cons_swap, forall_rel_cons_ext, card_pi, mem_pi, pi_cons, pi_zero	12
Total	15

Multiset

Definitions

Name	Category	Theorems
pi 📖	CompOp	8 math math: pi_cons, card_pi, mem_pi, MultilinearMap.dfinsuppFamily_apply_support', Nodup.pi, Finset.pi_val, pi_coe, pi_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_pi 📖	mathematical	—	card pi prod Nat.instCommMonoid map	—	induction_on card_singleton pi_cons card_bind map_congr card_map map_const' sum_replicate map_cons prod_cons
mem_pi 📖	mathematical	—	Multiset instMembership pi	—	induction_on notMem_zero pi_cons Pi.cons_same mem_cons Pi.cons_ne mem_cons_self mem_cons_of_mem Pi.cons_eta
pi_cons 📖	mathematical	—	pi cons bind map Pi.cons	—	recOn_cons
pi_zero 📖	mathematical	—	pi Multiset instZero instSingleton Pi.empty	—	—

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	Multiset.Nodup	Multiset.Nodup Multiset.pi	—	Multiset.induction_on Multiset.nodup_singleton Multiset.pi_cons map Multiset.Pi.cons_injective Multiset.mem_cons_of_mem pairwise Multiset.disjoint_map_map Multiset.mem_cons_self Multiset.Pi.cons_same

Multiset.Pi

Definitions

Name	Category	Theorems
cons 📖	CompOp	9 math math: Multiset.pi_cons, cons_swap, forall_rel_cons_ext, cons_coe, cons_map, cons_same, cons_ne, cons_eta, cons_injective
empty 📖	CompOp	1 math math: Multiset.pi_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_eta 📖	mathematical	—	cons Multiset.mem_cons_self Multiset.mem_cons_of_mem	—	Multiset.mem_cons_self Multiset.mem_cons_of_mem cons_same Multiset.mem_cons cons_ne
cons_injective 📖	mathematical	Multiset Multiset.instMembership	cons	—	Multiset.mem_cons_of_mem Multiset.mem_cons cons_ne
cons_map 📖	mathematical	—	cons	—	—
cons_ne 📖	mathematical	Multiset Multiset.instMembership Multiset.cons	cons Multiset Multiset.instMembership Multiset.cons Multiset.mem_cons	—	—
cons_same 📖	mathematical	Multiset Multiset.instMembership Multiset.cons	cons	—	—
cons_swap 📖	mathematical	—	cons Multiset.cons	—	Function.hfunext Multiset.cons_swap Decidable.ne_or_eq Decidable.eq_or_ne Multiset.mem_cons cons_ne cons_same
forall_rel_cons_ext 📖	mathematical	Multiset Multiset.instMembership Multiset.cons	cons	—	—

---

← Back to Index