Commit 2025-04-25 13:55 5fd096bd
View on Github →chore: use TreeMap in to_additive (#24366)
This PR avoids use of Lean.RBMap in the implementation of to_additive, where the new Std.TreeMap suffices.
chore: use TreeMap in to_additive (#24366)
This PR avoids use of Lean.RBMap in the implementation of to_additive, where the new Std.TreeMap suffices.