`IndisputableMonolith.Nuclear.NeutronStarEOSStructure`

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

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Nuclear.NuclearForceStructure
   3
   4namespace IndisputableMonolith
   5namespace Nuclear
   6namespace NeutronStarEOSStructure
   7
   8open NuclearForceStructure
   9
  10theorem has_nuclear_force_structure : nuclear_force_from_ledger := nuclear_force_structure
  11
  12def neutron_star_eos_from_ledger : Prop := nuclear_force_from_ledger
  13
  14theorem neutron_star_eos_structure : neutron_star_eos_from_ledger :=
  15  has_nuclear_force_structure
  16
  17/-- Neutron-star-EOS structure implies nuclear-force-side input. -/
  18theorem neutron_star_eos_implies_nuclear_force (h : neutron_star_eos_from_ledger) :
  19    nuclear_force_from_ledger :=
  20  h
  21
  22end NeutronStarEOSStructure
  23end Nuclear
  24end IndisputableMonolith
  25

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