theorem
other
other
rs_eta_33
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)
73theorem rs_eta_33 : rs_eta 3 3 = 1 := by simp [rs_eta]
depends on (2)
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