Commit 2024-07-15 18:29 2d6fcd30

View on Github →

chore: fix a typo in PolarCoord (#14767)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

added theorem Complex.polarCoord_symm_abs

deleted theorem Complex.polardCoord_symm_abs

Modified Mathlib/MeasureTheory/Integral/Gamma.lean