`cmb_temperature_now`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.CMBTemperature
domain: Physics
line: 149 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.CMBTemperature on GitHub at line 149.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

cmb_temperature IndisputableMonolith.Physics.CMBTemperature

formal source

 146  field_simp [hne]
 147
 148/-- At z = 0 (now): T = T₀. -/
 149theorem cmb_temperature_now (T₀ : ℝ) (hT₀ : 0 < T₀) :
 150    cmb_temperature T₀ 0 = T₀ := by
 151  unfold cmb_temperature
 152  simp
 153
 154end CMB
 155end Physics
 156end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.