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.

Estimated changes