mathlib
db9cb466 - feat(analysis/complex): equiv_real_prod_symm_apply (#15122)

Commit

3 years ago

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

Author

sgouezel

Parents