chore(data/real/pi): split into three files (#9295)

This is the last file to finish compilation in mathlib, and it naturally splits into three chunks, two of which have simpler dependencies. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Sep 20, 2021 · 3703ab2 · 3703ab2
1 parent 8c96c54
commit 3703ab2
Show file tree

Hide file tree

Showing 5 changed files with 378 additions and 356 deletions.
diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean
@@ -940,7 +940,7 @@ intermediate_value_Icc' (by norm_num) continuous_on_cos
   ⟨le_of_lt cos_two_neg, le_of_lt cos_one_pos⟩
 
 /-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from
-which one can derive all its properties. For explicit bounds on π, see `data.real.pi`. -/
+which one can derive all its properties. For explicit bounds on π, see `data.real.pi.bounds`. -/
 protected noncomputable def pi : ℝ := 2 * classical.some exists_cos_eq_zero
 
 localized "notation `π` := real.pi" in real

diff --git a/src/data/real/pi.lean b/src/data/real/pi.lean