Commit 2026-03-05 21:52 0ed793ff

View on Github →

chore(Analysis): golf using custom elaborators (#36199)

Estimated changes

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

modified theorem UpperHalfPlane.contMDiffAt_ofComplex

modified theorem UpperHalfPlane.contMDiff_coe

modified theorem UpperHalfPlane.contMDiff_denom

modified theorem UpperHalfPlane.contMDiff_denom_zpow

modified theorem UpperHalfPlane.contMDiff_inv_denom

modified theorem UpperHalfPlane.contMDiff_num

modified theorem UpperHalfPlane.contMDiff_smul

modified theorem UpperHalfPlane.eq_zero_of_frequently

modified theorem UpperHalfPlane.mdifferentiableAt_ofComplex

modified theorem UpperHalfPlane.mdifferentiable_coe

modified theorem UpperHalfPlane.mdifferentiable_denom

modified theorem UpperHalfPlane.mdifferentiable_denom_zpow

modified theorem UpperHalfPlane.mdifferentiable_inv_denom

modified theorem UpperHalfPlane.mdifferentiable_num

modified theorem UpperHalfPlane.mdifferentiable_smul

modified theorem UpperHalfPlane.mul_eq_zero_iff

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean