Commit 2024-06-26 06:40 c73f846b

View on Github →

chore: update Mathlib dependencies 2024-06-26 (#14145) This PR updates the Mathlib dependencies.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Data/BinaryHeap.lean

deleted def Array.heapSort

deleted def Array.toBinaryHeap

deleted def BinaryHeap.decreaseKey

deleted def BinaryHeap.empty

deleted def BinaryHeap.extractMax

deleted def BinaryHeap.get

deleted def BinaryHeap.heapifyDown

deleted def BinaryHeap.heapifyUp

deleted def BinaryHeap.increaseKey

deleted def BinaryHeap.insert

deleted def BinaryHeap.insertExtractMax

deleted def BinaryHeap.max

deleted def BinaryHeap.mkHeap

deleted def BinaryHeap.popMax

deleted def BinaryHeap.popMaxAux

deleted def BinaryHeap.replaceMax

deleted def BinaryHeap.singleton

deleted def BinaryHeap.size

deleted theorem BinaryHeap.size_heapifyDown

deleted theorem BinaryHeap.size_heapifyUp

deleted theorem BinaryHeap.size_insert

deleted theorem BinaryHeap.size_mkHeap

deleted theorem BinaryHeap.size_popMax

deleted theorem BinaryHeap.size_pos_of_max

deleted structure BinaryHeap

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Mathport/Notation.lean

Modified Mathlib/Tactic/Hint.lean

Modified Mathlib/Tactic/Says.lean

Modified lake-manifest.json