Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-14 13:57 375dd53e

View on Github →

refactor(geometry/manifold): split bump_function into 3 files (#8313) This is the a part of #8309. Both code and comments were moved with almost no modifications: added/removed variables/sections, slightly adjusted comments to glue them together.

Estimated changes