pith. machine review for the scientific record. sign in
theorem proved term proof

solar_angle_forced

show as:
view Lean formalization →

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)

  51theorem solar_angle_forced :
  52    solar_weight - solar_radiative_correction = phi ^ (-2 : ℤ) - 10 * Constants.alpha := by

proof body

Term-mode proof.

  53  unfold solar_weight solar_radiative_correction
  54  ring
  55
  56/-- The atmospheric mixing weight (maximal parity mix). -/

depends on (5)

Lean names referenced from this declaration's body.