def
definition
r_process_yields_from_ledger
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Nuclear.RProcessYieldsStructure on GitHub at line 12.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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