Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-05 15:04 db9cb466

View on Github →

feat(analysis/complex): equiv_real_prod_symm_apply (#15122) Plus some minor lemmas for #15106.

Estimated changes