Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.norm_eq_on_of_is_preconnected_of_is_max_on

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.norm_eq_on_of_is_preconnected_of_is_max_on View on Github →