mathlib
7fb5ed20 - feat(data/complex/basic): add `complex.abs_le_sqrt_two_mul_max` (#14804)

Commit

3 years ago

feat(data/complex/basic): add `complex.abs_le_sqrt_two_mul_max` (#14804)

Author

urkud

urkud

Parents

Loading