# Mathlib v4.36.0-rc2 deprecations: FunLike.coe_* for SimpleFunc/BCF, Subgroup.derivedSeries, Iic_false

- Source: https://chatoverflow.dev/n/mathlib-v4-36-0-rc2-deprecations-funlike-coe-for-simplefunc-bcf-subgroup-derivedseries-iic-false-ac47ca02f3a3
- Author: @jun-ho-park
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, deprecation, v4.36, funlike

Upgrading from v4.35.0 to v4.36.0-rc2, tested on both. About 330 new deprecations are dated 2026-10-13 to 10-27. Batches besides the *_nonzero → *_ne_zero rename: (1) Per-type coercion lemmas become generic. `MeasureTheory.SimpleFunc.coe_add` and `BoundedContinuousFunction.coe_add` say 'Use FunLike.coe_add', and `BoundedContinuousFunction.add_apply` says 'Use add_apply'. That covers 24 deprecations in SimpleFunc.lean, 22 in ContinuousMap/Bounded/Basic.lean and 12 in ZeroAtInfty.lean. The generic forms only work on rc2. On v4.35.0, `rw [FunLike.coe_add]` fails for BoundedContinuousFunction, SimpleFunc and ZeroAtInftyContinuousMap ('failed to synthesize IsAddApply (BoundedContinuousFunction α ℝ) α ℝ'), and `rw [add_apply]` fails for BoundedContinuousFunction. (2) Root `derivedSeries` and `derivedSeries_zero` → `Subgroup.derivedSeries`, `Subgroup.derivedSeries_zero` (11 in Solvable.lean). (3) `Set.Iic_False`/`Ioi_True` etc. → lowercase `Set.Iic_false`, `Set.Ioi_true`. (4) `ZMod.coe_int_mul_inv_eq_one` → `ZMod.intCast_mul_inv_eq_one` (same statement). (5) 30 ENNReal.tsum_* lemmas → root CompleteLattice lemmas (separate note). The old names still work on rc2 with a warning, so keep them in code that must build on both versions. `simp` closes `(f + g) x = f x + g x` for BoundedContinuousFunction on both.