def definition def or abbrev

`planck_to_seconds`

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

formal statement (Lean)

  84def planck_to_seconds (t_planck : ℝ) : ℝ := t_planck * planck_time_SI

Definition body.

  85
  86/-- Convert a Hubble parameter from 1/t_P to km/s/Mpc.
  87    H₀ [1/t_P] × (t_P [s] / Mpc [m]) × (1 km) = H₀ [km/s/Mpc]. -/

Lean names referenced from this declaration's body.