pith. machine review for the scientific record. sign in
theorem proved term proof

optical_reduces_to_gr

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  61theorem optical_reduces_to_gr (z : ℝ) (bg_DA : ℝ) (P : ILG.KernelParams)
  62    (hC : P.C = 0) :
  63    DA_rescaled z bg_DA P = bg_DA := by

proof body

Term-mode proof.

  64  unfold DA_rescaled Upsilon
  65  simp [hC]
  66
  67end Cosmology
  68end Relativity
  69end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.