lemma proved term proof

`planck_time_pos`

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

formal statement (Lean)

 158lemma planck_time_pos : 0 < planck_time := by

Term-mode proof.

 159  unfold planck_time
 160  exact sqrt_pos.mpr (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 5))
 161

Lean names referenced from this declaration's body.