`neutron_lifetime_discrepancy_structure`

proved

show as: view math explainer →

module: IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure
domain: Experimental
line: 15 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Experimental.NeutronLifetimeDiscrepancyStructure on GitHub at line 15.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

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