Commit 2025-07-05 17:25 ba1ca766

View on Github →

chore: clean up and remove FunProp/Differentiable (#26404)

  • one lemma in that file already exists, hence can be removed (We don't add a deprecation as I presume people will not have used it.)
  • move the three remaining lemmas in that file to their proper place, and use the now fun_ naming convention (Omitting deprecations again.)
  • after this, FunProp/Differentiable is empty and need not be imported any more: add a module deprecation

Estimated changes

deleted theorem Differentiable.comp'
deleted theorem DifferentiableAt.comp'
deleted theorem DifferentiableOn.comp'
deleted theorem differentiableOn_id'