mathlib3
f471b899 - feat(topology,geometry/manifold): continuous and smooth partition of unity (#8281)
