Commit 2024-10-15 10:13 c9428b0d

chore: split off RBMap dependency from Mathlib.Data.Tree (#17764) Tree.ofRBNode does not seem to be used in Mathlib anyway, so let's avoid an unnecessary import of Batteries and move this to a new leaf file in case anyone needs to use it still.