Commit 2026-11-02 15:00 74d53835

chore(Geometry/Manifold/VectorBundle): rename iff lemmas about differentiability to mention iff (#45588) All these lemmas characterise differentiability using a trivialization, hence could mention iff as part of their name. They should, since there exist conceivable statements of the same name without the iff (e.g., about some section being differentiable). This also increases naming consistency: a number of similar lemmas in that file already use the iff naming. Zulip discussion supporting this: #mathlib4 > Naming convention @ 💬