theorem other other

`rs_eta_00`

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

formal statement (Lean)

  70theorem rs_eta_00 : rs_eta 0 0 = -1 := by simp [rs_eta]

Lean names referenced from this declaration's body.

rs_eta in IndisputableMonolith.Physics.CMBTemperature decl_use
rs_eta in IndisputableMonolith.Relativity.Geometry.MetricUnification decl_use