mathlib3

a44c9a18 - chore(*): protect some definitions to get rid of _root_ (#2846)

chore(*): protect some definitions to get rid of _root_ (#2846) These were amongst the worst offenders. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>