`IndisputableMonolith.Support.Powers`

IndisputableMonolith/Support/Powers.lean · 24 lines · 1 declarations

Explainer status: ready · generated 2026-05-13 03:02:48.260984+00:00

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Support
   6
   7open Constants
   8
   9/-- phi^(0:ℤ) = 1 as a convenience lemma for integer powers of φ. -/
  10lemma phi_zpow_zero : phi ^ (0 : ℤ) = (1 : ℝ) := by
  11  simpa using (zpow_zero (phi : ℝ))
  12
  13end Support
  14end IndisputableMonolith
  15
  16
  17
  18
  19
  20
  21
  22
  23
  24

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