Commit 2022-09-24 14:07 ba80091d

View on Github →

feat(data/complex/basic): bundle complex.abs (#16347) Doing this this way round makes the refactor in #16340 much easier. I will follow up this PR with similar PRs for padic_norm and padic_norm_e.

Estimated changes

Modified src/algebra/order/absolute_value.lean

added theorem absolute_value.coe_mk

Modified src/analysis/complex/basic.lean

Modified src/analysis/complex/circle.lean

Modified src/analysis/complex/isometry.lean

Modified src/analysis/complex/phragmen_lindelof.lean

Modified src/analysis/complex/polynomial.lean

Modified src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean

Modified src/analysis/special_functions/compare_exp.lean

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

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

Modified src/analysis/special_functions/gamma.lean

Modified src/analysis/special_functions/polar_coord.lean

Modified src/analysis/special_functions/pow.lean

Modified src/data/complex/basic.lean

deleted theorem complex.abs_abs_sub_le_abs_sub

deleted theorem complex.abs_add

added theorem complex.abs_apply

modified theorem complex.abs_conj

added theorem complex.abs_def

deleted theorem complex.abs_div

deleted theorem complex.abs_eq_zero

deleted theorem complex.abs_inv

deleted theorem complex.abs_mul

deleted theorem complex.abs_ne_zero

deleted theorem complex.abs_neg

deleted theorem complex.abs_nonneg

deleted theorem complex.abs_one

deleted theorem complex.abs_pos

deleted theorem complex.abs_sub_comm

deleted theorem complex.abs_sub_le

added theorem complex.abs_theory.abs_conj

deleted theorem complex.abs_zero

Modified src/data/complex/exponential.lean

Modified src/geometry/euclidean/oriented_angle.lean

Modified src/measure_theory/integral/circle_integral.lean

Modified src/measure_theory/integral/circle_transform.lean

Modified src/number_theory/l_series.lean

Modified src/number_theory/modular.lean

Modified src/ring_theory/polynomial/cyclotomic/eval.lean