`r_process_yields_structure`

proved

show as: view math explainer →

module: IndisputableMonolith.Nuclear.RProcessYieldsStructure
domain: Nuclear
line: 14 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Nuclear.RProcessYieldsStructure on GitHub at line 14.

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

formal source

  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

papers checked against this theorem

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