Open bryangingechen opened 3 months ago
No significant changes to the import graph
No declarations were harmed in the making of this PR! 🐙
The doc-module for script/declarations_diff.sh
contains some details about this script.
bors delegated
bors d
bors r+
This PR updates the Mathlib dependencies.