OffDiag

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

Statistics

Metric	Count
Definitions offDiag	1
Theorems mem_offDiag, of_offDiag, offDiag, offDiag, count_offDiag_eq_mul_sub_ite, length_offDiag, length_offDiag', map_prodMap_offDiag, mem_offDiag_iff_getElem, nodup_offDiag, offDiag_cons_perm, offDiag_nil, offDiag_singleton	13
Total	14

List

Definitions

Name	Category	Theorems
offDiag 📖	CompOp	12 math math: count_offDiag_eq_mul_sub_ite, length_offDiag, map_prodMap_offDiag, offDiag_singleton, nodup_offDiag, offDiag_nil, length_offDiag', Nodup.offDiag, Nodup.mem_offDiag, mem_offDiag_iff_getElem, Perm.offDiag, offDiag_cons_perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_offDiag_eq_mul_sub_ite 📖	mathematical	—	offDiag	—	count_map_of_injective offDiag_cons_perm
length_offDiag 📖	mathematical	—	offDiag	—	length_offDiag'
length_offDiag' 📖	mathematical	—	offDiag	—	—
map_prodMap_offDiag 📖	mathematical	—	offDiag	—	eraseIdx_map
mem_offDiag_iff_getElem 📖	mathematical	—	offDiag	—	—
nodup_offDiag 📖	mathematical	—	offDiag	—	Nodup.of_offDiag Nodup.offDiag
offDiag_cons_perm 📖	mathematical	—	offDiag	—	map_append_flatMap_perm
offDiag_nil 📖	mathematical	—	offDiag	—	—
offDiag_singleton 📖	mathematical	—	offDiag	—	—

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_offDiag 📖	mathematical	—	List.offDiag	—	getElem_inj_iff
of_offDiag 📖	—	List.offDiag	—	—	Mathlib.Tactic.Contrapose.contrapose₁ List.count_offDiag_eq_mul_sub_ite
offDiag 📖	mathematical	—	List.offDiag	—	List.nodup_iff_count_le_one List.count_offDiag_eq_mul_sub_ite

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
offDiag 📖	mathematical	—	List.offDiag	—	List.count_offDiag_eq_mul_sub_ite

---

← Back to Index