Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.eq_of_is_max_on_of_ball_subset

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_of_is_max_on_of_ball_subsetView on Github →