`IndisputableMonolith.Nuclear.RProcessYieldsStructure`

IndisputableMonolith/Nuclear/RProcessYieldsStructure.lean · 25 lines · 4 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Nuclear.NeutronStarEOSStructure
   3
   4namespace IndisputableMonolith
   5namespace Nuclear
   6namespace RProcessYieldsStructure
   7
   8open NeutronStarEOSStructure
   9
  10theorem has_ns_eos_structure : neutron_star_eos_from_ledger := neutron_star_eos_structure
  11
  12def r_process_yields_from_ledger : Prop := neutron_star_eos_from_ledger
  13
  14theorem r_process_yields_structure : r_process_yields_from_ledger :=
  15  has_ns_eos_structure
  16
  17/-- R-process-yields structure implies neutron-star-EOS-side input. -/
  18theorem r_process_implies_ns_eos (h : r_process_yields_from_ledger) :
  19    neutron_star_eos_from_ledger :=
  20  h
  21
  22end RProcessYieldsStructure
  23end Nuclear
  24end IndisputableMonolith
  25

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