Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.eq_on_of_is_preconnected_of_is_max_on_norm

Modification history

2022-07-17 04:14
src/analysis/complex/abs_max.lean
feat(analysis/complex/abs_max): add a version of the maximum modulus principle (#15364) …
Added complex.eq_on_of_is_preconnected_of_is_max_on_normView on Github →