`has_nuclear_force_structure`

proved

show as: view math explainer →

module: IndisputableMonolith.Nuclear.NeutronStarEOSStructure
domain: Nuclear
line: 10 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Nuclear.NeutronStarEOSStructure on GitHub at line 10.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

   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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.