theorem
proved
has_neutron_lifetime_input
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure on GitHub at line 10.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
7
8open Nuclear.NeutronLifetimeStructure
9
10theorem has_neutron_lifetime_input : neutron_lifetime_from_ledger :=
11 neutron_lifetime_structure
12
13def neutron_lifetime_discrepancy_from_ledger : Prop := neutron_lifetime_from_ledger
14
15theorem neutron_lifetime_discrepancy_structure :
16 neutron_lifetime_discrepancy_from_ledger := has_neutron_lifetime_input
17
18/-- Neutron-lifetime-discrepancy structure implies neutron-lifetime input. -/
19theorem neutron_discrepancy_implies_lifetime_input
20 (h : neutron_lifetime_discrepancy_from_ledger) :
21 neutron_lifetime_from_ledger :=
22 h
23
24end NeutronLifetimeDiscrepancyStructure
25end Experimental
26end IndisputableMonolith