FinRange

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

Statistics

Metric	Count
Definitions	0
Theorems map_finRange_perm, ofFn_comp_perm, count_finRange, finRange_eq_nil, finRange_map_get, finRange_map_getElem, finRange_succ_eq_map, idxOf_finRange, map_coe_finRange, nodup_ofFn, nodup_ofFn_ofInjective, ofFn_eq_map, ofFn_eq_pmap, ofFn_id	14
Total	14

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_finRange_perm 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	List.Nodup.map Equiv.injective Equiv.surjective
ofFn_comp_perm 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	List.ofFn_eq_map map_finRange_perm

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_finRange 📖	—	—	—	—	instLawfulBCmpCompare_mathlib
finRange_eq_nil 📖	—	—	—	—	—
finRange_map_get 📖	—	—	—	—	—
finRange_map_getElem 📖	—	—	—	—	—
finRange_succ_eq_map 📖	—	—	—	—	—
idxOf_finRange 📖	—	—	—	—	instLawfulBCmpCompare_mathlib
map_coe_finRange 📖	—	—	—	—	—
nodup_ofFn 📖	—	—	—	—	Function.injective_of_subsingleton Fin.cons_injective_iff Fin.cons_zero Fin.cons_succ nodup_ofFn_ofInjective
nodup_ofFn_ofInjective 📖	—	—	—	—	ofFn_eq_pmap Nodup.pmap
ofFn_eq_map 📖	—	—	—	—	ofFn_id map_ofFn
ofFn_eq_pmap 📖	—	—	—	—	—
ofFn_id 📖	—	—	—	—	—

---

← Back to Index