Commit 2024-12-17 18:11 9890d5ff

View on Github →

feat(Analysis/PolarCoord): add versions for Lebesgue integral (#18490) This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

added theorem Complex.measurableEquivRealProd_symm_polarCoord_symm_apply

added theorem det_fderiv_polarCoord_symm

added theorem lintegral_comp_polarCoord_symm