theorem other other

`rs_eta_11`

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

formal statement (Lean)

  71theorem rs_eta_11 : rs_eta 1 1 = 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