module module

`IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (8)

def F L64
def W L67
def dim L70
def tauStepCoefficientDerived L76
theorem tauStepCoefficientDerived_eq L80
theorem tauStepCoefficientDerived_matches_paper L85
def stepMuTauDerived L93
theorem stepMuTauDerived_matches_def L97