`IndisputableMonolith.Astrophysics.SupernovaMechanismStructure`

IndisputableMonolith/Astrophysics/SupernovaMechanismStructure.lean · 22 lines · 3 declarations

Explainer status: ready · generated 2026-05-15 01:50:23.138769+00:00

   1import Mathlib
   2import IndisputableMonolith.Astrophysics.StellarIMFStructure
   3
   4namespace IndisputableMonolith
   5namespace Astrophysics
   6namespace SupernovaMechanismStructure
   7
   8open StellarIMFStructure
   9
  10def supernova_mechanism_from_ledger : Prop := stellar_imf_from_ledger
  11
  12theorem supernova_mechanism_structure : supernova_mechanism_from_ledger := stellar_imf_structure
  13
  14/-- Supernova-mechanism structure implies IMF-side structural input. -/
  15theorem supernova_implies_stellar_imf (h : supernova_mechanism_from_ledger) :
  16    stellar_imf_from_ledger :=
  17  h
  18
  19end SupernovaMechanismStructure
  20end Astrophysics
  21end IndisputableMonolith
  22

source mirrored from github.com/jonwashburn/shape-of-logic