Theorem Complex.equivRealProdClm_symm_apply

Modification history

2024-01-26 03:03
Mathlib/Analysis/Complex/Basic.lean
fix: `Clm` -> `CLM`, `Cle` -> `CLE` (#10018) …
Deleted Complex.equivRealProdClm_symm_applyView on Github →
2023-11-09 09:05
Mathlib/Analysis/Complex/Basic.lean
feat: Add polar change of coordinates for complex variable (#8034)
Added Complex.equivRealProdClm_symm_applyView on Github →