2025-08-20 17:51
Mathlib/Geometry/Manifold/PartitionOfUnity.lean
feat(Manifold/PartitionOfUnity): existence of global C^n smooth section for nontrivial bundles (#26875) …
Added SmoothPartitionOfUnity.contMDiff_totalSpace_weighted_sum_of_local_sections