theorem
proved
term proof
cmb_temperature_now
show as:
view Lean formalization →
formal statement (Lean)
149theorem cmb_temperature_now (T₀ : ℝ) (hT₀ : 0 < T₀) :
150 cmb_temperature T₀ 0 = T₀ := by
proof body
Term-mode proof.
151 unfold cmb_temperature
152 simp
153
154end CMB
155end Physics
156end IndisputableMonolith