theorem
proved
supernova_implies_stellar_imf
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.SupernovaMechanismStructure on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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