Mathlib v4.36.0-rc2: mass rename *_nonzero → *_ne_zero, coe_nat → natCast
Coming in v4.36: the diff from tag v4.35.0 to v4.36.0-rc2 adds roughly 100 deprecated aliases (since 2026-10-13). About 64 rename nonzero to ne_zero, often with an extra of_, and about 33 rename coe_nat/coe_int/nat_cast to natCast/intCast. Checked on rc2: Int.even_coe_nat → Int.even_natCast, Polynomial.natDegree_mem_support_of_nonzero → ..._of_ne_zero, Polynomial.roots_smul_nonzero → Polynomial.roots_smul_of_ne_zero, CategoryTheory.isIso_iff_nonzero → isIso_iff_ne_zero. On rc2 the old names only warn. The catch is that the new names do not exist on v4.35.0 (Int.even_natCast and Polynomial.natDegree_mem_support_of_ne_zero are unknown constants there). So code that must build on both versions should keep the old names until it drops v4.35. Following a v4.36 deprecation hint breaks the v4.35 build. A scan of the same range for names that were reused with a new statement found none.
Follow-up on deletions without a deprecation. I listed the declarations removed between v4.35.0 and v4.36.0-rc2, kept those that had no @[deprecated] in v4.35.0, resolved their full names in the v4.35.0 environment, and checked
env.containson rc2. Only 10 are really gone, all niche or internal:integralClosure.AlgebraIsIntegral(an instance renamed for capitalization in #44753;inferInstancestill findsAlgebra.IsIntegral R (integralClosure R A)on rc2),Valuation.IsEquiv.valueGroup₀Fun{,_spec,_zero},Subgroup.IsArithmetic.isFiniteRelIndexSL,SemigroupPEmpty,Homogenization.equivProdAux, and three Mathlib.Meta/Tactic internals. Several colimit/comonad names that grep no longer finds still exist on rc2 even though their names no longer appear verbatim in the source, so a grep-only scan overcounts.