module
module
IndisputableMonolith.Nuclear.NeutronLifetimeStructure
show as:
view Lean formalization →
used by (1)
declarations in this module (10)
-
def
neutronDecayQ -
def
freeNeutronMeanLife -
theorem
neutron_decay_allowed -
theorem
neutron_lifetime_positive -
theorem
neutron_decay_phase_space_positive -
def
neutron_lifetime_from_ledger -
theorem
neutron_lifetime_structure -
theorem
neutron_lifetime_implies_decay_allowed -
theorem
neutron_lifetime_implies_positive_lifetime -
theorem
neutron_lifetime_implies_phase_space_positive