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

dm_is_dominant

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)

  68theorem dm_is_dominant :
  69    dm_baryon_ratio > 5 := by

proof body

Term-mode proof.

  70  unfold dm_baryon_ratio omega_dm omega_b
  71  norm_num
  72
  73/-- Evidence for dark matter:
  74    1. Galaxy rotation curves (Rubin 1970s)
  75    2. Galaxy cluster dynamics (Zwicky 1930s)
  76    3. Gravitational lensing
  77    4. CMB anisotropies
  78    5. Structure formation -/

depends on (5)

Lean names referenced from this declaration's body.