Pi

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

Statistics

Metric	Count
Definitions cons, head, nil, tail, pi	5
Theorems cons_def, cons_eta, cons_map, forall_rel_cons_ext, mem_pi, pi_cons, pi_nil, cons_coe, pi_coe	9
Total	14

List

Definitions

Name	Category	Theorems
pi 📖	CompOp	5 math math: mem_pi, mem_pi_toList, pi_cons, Multiset.pi_coe, pi_nil

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_pi 📖	mathematical	—	pi	—	Multiset.pi_coe Multiset.mem_pi
pi_cons 📖	mathematical	—	pi Pi.cons	—	—
pi_nil 📖	mathematical	—	pi Pi.nil	—	—

List.Pi

Definitions

Name	Category	Theorems
cons 📖	CompOp	6 math math: cons_eta, cons_def, Multiset.Pi.cons_coe, cons_map, List.pi_cons, forall_rel_cons_ext
head 📖	CompOp	1 math math: cons_eta
nil 📖	CompOp	1 math math: List.pi_nil
tail 📖	CompOp	1 math math: cons_eta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_def 📖	mathematical	—	cons	—	—
cons_eta 📖	mathematical	—	cons head tail	—	Multiset.Pi.cons_eta
cons_map 📖	mathematical	—	cons	—	Multiset.Pi.cons_map
forall_rel_cons_ext 📖	mathematical	—	cons	—	Multiset.Pi.forall_rel_cons_ext

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_coe 📖	mathematical	—	pi ofList List.pi	—	pi_cons map_congr coe_bind

Multiset.Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_coe 📖	mathematical	—	cons Multiset.ofList List.Pi.cons	—	—

---

← Back to Index