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

Modified src/analysis/special_functions/complex/arg.lean

added theorem complex.arg_lt_pi_iff

Modified src/analysis/special_functions/pow.lean

added theorem real.continuous_at_rpow_const

Modified src/data/complex/basic.lean

modified def complex.equiv_real_prod

added theorem complex.equiv_real_prod_symm_apply

Modified src/topology/separation.lean

added theorem is_open_ne_fun