Commit 2026-03-05 11:23 3e8515c6

View on Github →

chore(Geometry/Manifold/Algebra): golf using custom elaborators (#36007)

Estimated changes

modified theorem ContMDiff.div
modified theorem ContMDiff.div₀
modified theorem ContMDiff.inv
modified theorem ContMDiff.inv₀
modified theorem ContMDiffAt.div
modified theorem ContMDiffAt.div₀
modified theorem ContMDiffAt.inv
modified theorem ContMDiffAt.inv₀
modified theorem ContMDiffOn.div
modified theorem ContMDiffOn.div₀
modified theorem ContMDiffOn.inv
modified theorem ContMDiffOn.inv₀
modified theorem ContMDiffWithinAt.inv₀
modified theorem contMDiffOn_inv₀
modified theorem contMDiff_inv
modified theorem ContMDiff.div_const
modified theorem ContMDiff.mul
modified theorem ContMDiff.pow
modified theorem ContMDiff.prod
modified theorem ContMDiffAt.prod
modified theorem ContMDiffOn.div_const
modified theorem ContMDiffOn.mul
modified theorem ContMDiffOn.pow
modified theorem ContMDiffWithinAt.div_const
modified theorem ContMDiffWithinAt.mul
modified theorem ContMDiffWithinAt.pow
modified theorem ContMDiffWithinAt.prod
modified theorem contMDiffAt_finset_prod'
modified theorem contMDiffAt_finset_prod
modified theorem contMDiffAt_mul_left
modified theorem contMDiffAt_mul_right
modified theorem contMDiffOn_finset_prod'
modified theorem contMDiffOn_finset_prod
modified theorem contMDiff_finprod
modified theorem contMDiff_finprod_cond
modified theorem contMDiff_finset_prod'
modified theorem contMDiff_finset_prod
modified theorem contMDiff_mul
modified theorem contMDiff_mul_left
modified theorem contMDiff_mul_right
modified theorem contMDiff_pow
modified theorem mdifferentiableAt_mul_left
modified theorem mdifferentiableAt_mul_right
modified theorem mdifferentiable_mul_left
modified theorem mdifferentiable_mul_right