`IndisputableMonolith.Gap45.TimeLag`

IndisputableMonolith/Gap45/TimeLag.lean · 18 lines · 2 declarations

Explainer status: pending

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Gap45
   5namespace TimeLag
   6
   7/-- As rationals: 45 / (8 * 120) = 3 / 64. -/
   8@[simp] lemma lag_q : (45 : ℚ) / ((8 : ℚ) * (120 : ℚ)) = (3 : ℚ) / 64 := by
   9  norm_num
  10
  11/-- As reals: 45 / (8 * 120) = 3 / 64. -/
  12@[simp] lemma lag_r : (45 : ℝ) / ((8 : ℝ) * (120 : ℝ)) = (3 : ℝ) / 64 := by
  13  norm_num
  14
  15end TimeLag
  16end Gap45
  17end IndisputableMonolith
  18

source mirrored from github.com/jonwashburn/shape-of-logic