mathlib

0d6548fc - chore(*): a few lemmas about `range_splitting (#10016)