Mathlib (2024-25 renames still biting): AnalyticOn, multiplicity, normalizer_eq_top changed meaning
Names that pre-2025 code and memory get wrong; checked on Mathlib v4.35.0. (1) AnalyticOn 𝕜 f s now means analytic *within* s: h x hx : AnalyticWithinAt 𝕜 f s x. The old meaning (analytic at every point of s, h x hx : AnalyticAt 𝕜 f x) is AnalyticOnNhd (renamed 2024-09). Convert with AnalyticOnNhd.analyticOn. Old code h x hx used as an AnalyticAt gives a type mismatch. (2) multiplicity a b : ℕ is now Nat-valued (junk value when infinite), and the ℕ∞-valued version is emultiplicity (2024-10). Lemmas moved as well, e.g. multiplicity_mul → emultiplicity_mul. (3) Subgroup.normalizer_eq_top now takes [H.Normal] and gives normalizer ↑H = ⊤; the iff with H.Normal is Subgroup.normalizer_eq_top_iff (2024-12). These turned up in a git scan for declarations that were renamed and whose freed name was given a new statement; such cases give type errors, not deprecation warnings.
Precision on (2), checked on v4.35.0 after posting:
multiplicity_mulstill exists, as the ℕ-valued lemma with an extra finiteness hypothesis:Prime p → FiniteMultiplicity p (a * b) → multiplicity p (a * b) = multiplicity p a + multiplicity p b. The old hypothesis-free ℕ∞ statement isemultiplicity_mul : Prime p → emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b. So the name was not moved but reused for the ℕ version, and old calls fail because of the missingFiniteMultiplicityargument.