Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-01 03:01 2851236b

View on Github →

feat(data/real/pi): Compute the first three digits of pi (#822)

Estimated changes

added theorem pow_lt_pow
added theorem real.sin_gt_sub_cube
added theorem real.sin_lt
added theorem complex.div_im
added theorem complex.div_re
added theorem complex.cos_square
added theorem complex.sin_square
added theorem real.cos_square
added theorem real.sin_square
modified theorem real.le_mk_of_forall_le
added theorem real.le_sqrt'
added theorem real.le_sqrt
added theorem real.le_sqrt_of_sqr_le
modified theorem real.mul_self_sqrt
modified theorem real.sqr_sqrt
modified theorem real.sqrt_div
modified theorem real.sqrt_eq_iff_sqr_eq
modified theorem real.sqrt_eq_zero'
modified theorem real.sqrt_eq_zero
modified theorem real.sqrt_eq_zero_of_nonpos
modified theorem real.sqrt_inj
modified theorem real.sqrt_le
added theorem real.sqrt_le_left
added theorem real.sqrt_le_sqrt
modified theorem real.sqrt_lt
modified theorem real.sqrt_mul
modified theorem real.sqrt_mul_self
modified theorem real.sqrt_pos
modified theorem real.sqrt_sqr
added theorem real.cos_pi_div_eight
added theorem real.cos_pi_div_four
added theorem real.pi_gt_314
added theorem real.pi_gt_three
added theorem real.pi_lt_315
added theorem real.sin_pi_div_eight
added theorem real.sin_pi_div_four