Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.eventually_eq_of_is_local_max_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.eventually_eq_of_is_local_max_normView on Github →