mathlib3
d107d825 - feat(data/complex): numerical bounds on log 2 (#7146)

Commit
4 years ago
feat(data/complex): numerical bounds on log 2 (#7146) Upper and lower bounds on log 2. Presumably these could be made faster but I don't know the tricks - the proof of `log_two_near_10` (for me) doesn't take longer than `exp_one_near_20` to compile. I also strengthened the existing bounds slightly.
Author
Parents
Loading