theorem proved term proof

`stellar_imf_implies_uhecr`

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

formal statement (Lean)

  15theorem stellar_imf_implies_uhecr (h : stellar_imf_from_ledger) : uhecr_from_ledger :=

Term-mode proof.

  16  h
  17
  18end StellarIMFStructure
  19end Astrophysics
  20end IndisputableMonolith

Lean names referenced from this declaration's body.

stellar_imf_from_ledger in IndisputableMonolith.Astrophysics.StellarIMFStructure decl_use
uhecr_from_ledger in IndisputableMonolith.Astrophysics.UHECRStructure decl_use