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

gravArea_inv_sq

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)

  60theorem gravArea_inv_sq (G_N M a c : ℝ) (_hc : 0 < c) (_ha : 0 < a) :
  61    gravArea G_N M (c * a) = gravArea G_N M a / c ^ 2 := by

proof body

Term-mode proof.

  62  unfold gravArea
  63  ring
  64
  65/-! ## §2. Dynamical Time and Demanded Rate -/
  66
  67/-- Keplerian dynamical time at radius r for mass M:
  68    T_dyn = 2π√(r³/(GM)). -/

depends on (8)

Lean names referenced from this declaration's body.