module
module
IndisputableMonolith.Physics.NeutronGFactorScoreCard
show as:
view Lean formalization →
depends on (1)
declarations in this module (11)
-
def
row_neutron_g_codata -
def
row_neutron_mu_over_muN_codata -
def
NeutronGFactorResidual -
theorem
row_neutron_g_codata_negative -
theorem
row_neutron_mu_codata_negative -
theorem
row_neutron_magnetic_cost_matched -
theorem
row_neutron_magnetic_cost_nonneg -
theorem
row_neutron_threshold_pos -
theorem
row_neutron_g_residual_named -
structure
NeutronGFactorScoreCardCert -
theorem
neutronGFactorScoreCardCert_holds