Commit 2025-01-21 17:14 69e7baf1

View on Github →

feat(Integral/Pi): a version of polarCoord for pi integrals (#18400) This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

added theorem abs_fst_of_mem_pi_polarCoord_target

added theorem det_fderivPiPolarCoordSymm

added theorem det_fderivPolarCoordSymm

deleted theorem det_fderiv_polarCoord_symm

added def fderivPolarCoordSymm

added theorem hasFDerivAt_pi_polarCoord_symm

added theorem injOn_pi_polarCoord_symm

added theorem integral_comp_pi_polarCoord_symm

added theorem lintegral_comp_pi_polarCoord_symm

added theorem measurableSet_pi_polarCoord_target

added theorem pi_polarCoord_symm_target_ae_eq_univ

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem LinearMap.det_pi

Modified Mathlib/Topology/Algebra/Module/Determinant.lean

added theorem ContinuousLinearMap.det_pi