Commit 2021-02-04 18:03 49cf0be5

View on Github →

refactor(real): protect real.pi (#6039) Currently, real.pi is not protected. This can conflict with set.pi. Since it is most often used as π through the real locale, let's protect it.

Estimated changes

Modified src/analysis/complex/roots_of_unity.lean

modified theorem complex.is_primitive_root_exp

Modified src/analysis/special_functions/trigonometric.lean

modified theorem real.cos_pi_div_eight

modified theorem real.cos_pi_div_four

modified theorem real.cos_pi_div_sixteen

modified theorem real.cos_pi_div_thirty_two

modified theorem real.cos_pi_over_two_pow

modified theorem real.sin_pi_div_eight

modified theorem real.sin_pi_div_four

modified theorem real.sin_pi_div_sixteen

modified theorem real.sin_pi_div_thirty_two

Modified src/data/real/pi.lean

modified theorem real.pi_gt_3141592

modified theorem real.pi_gt_31415

modified theorem real.pi_gt_314

modified theorem real.pi_gt_sqrt_two_add_series

modified theorem real.pi_gt_three

modified theorem real.pi_lt_3141593

modified theorem real.pi_lt_31416

modified theorem real.pi_lt_315