Documentation Verification Report

Sort

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

Statistics

Metric	Count
Definitions `instRepr`, `instToExprOfToLevel`, `sort`	3
Theorems `coe_sort`, `length_sort`, `map_sort`, `mem_sort`, `pairwise_sort`, `sort_cons`, `sort_eq`, `sort_range`, `sort_singleton`, `sort_sorted`, `sort_zero`	11
Total	14

Multiset

Definitions

Name	Category	Theorems
`instRepr` 📖	CompOp	—
`instToExprOfToLevel` 📖	CompOp	—
`sort` 📖	CompOp	14 math math: `map_sort`, `sort_cons`, `sort_sorted`, `Finset.sort_mk`, `sort_zero`, `Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀`, `mem_sort`, `length_sort`, `coe_sort`, `sort_eq`, `sort_singleton`, `pairwise_sort`, `sort_range`, `Finset.sort_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_sort` 📖	mathematical	—	`sort` `ofList`	—	—
`length_sort` 📖	mathematical	—	`sort` `card`	—	—
`map_sort` 📖	mathematical	—	`sort` `map`	—	—
`mem_sort` 📖	mathematical	—	`sort` `Multiset` `instMembership`	—	`mem_coe` `sort_eq`
`pairwise_sort` 📖	mathematical	—	`sort`	—	`List.pairwise_mergeSort'`
`sort_cons` 📖	mathematical	—	`sort` `cons`	—	`List.mergeSort_eq_insertionSort` `List.insertionSort_cons` `List.insertionSort_cons_of_forall_rel`
`sort_eq` 📖	mathematical	—	`ofList` `sort`	—	—
`sort_range` 📖	mathematical	—	`sort` `range` `instIsTransLe` `Nat.instPreorder` `LE.total` `Nat.instLinearOrder`	—	`List.mergeSort_eq_self` `LE.total` `instIsTransLe` `List.SortedLE.pairwise` `List.SortedLT.sortedLE` `List.sortedLT_range`
`sort_singleton` 📖	mathematical	—	`sort` `Multiset` `instSingleton`	—	—
`sort_sorted` 📖	mathematical	—	`sort`	—	`pairwise_sort`
`sort_zero` 📖	mathematical	—	`sort` `Multiset` `instZero`	—	—

---

← Back to Index