Commit 2023-11-09 09:05 376952a5

View on Github →

feat: Add polar change of coordinates for complex variable (#8034)

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.equivRealProdClm_symm_apply

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

added theorem Complex.polardCoord_symm_abs

Modified Mathlib/Data/Complex/Module.lean

added theorem Complex.equivRealProdAddHom_symm_apply

added theorem Complex.equivRealProdLm_symm_apply

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean