Commit 2023-06-08 08:49 68981308

View on Github →

feat: port Analysis.SpecialFunctions.PolarCoord (#4848)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

added theorem hasFDerivAt_polarCoord_symm

added theorem integral_comp_polarCoord_symm

added def polarCoord

added theorem polarCoord_source_ae_eq_univ