pith. machine review for the scientific record. sign in
def definition def or abbrev

electroweakMassBridgeCert

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

formal statement (Lean)

 195def electroweakMassBridgeCert : ElectroweakMassBridgeCert where
 196  mW_sq_nn         := mW_sq_nonneg

proof body

Definition body.

 197  mZ_sq_nn         := mZ_sq_nonneg
 198  mW_le_mZ         := mW_sq_le_mZ_sq
 199  mW_lt_mZ         := fun g gp v hgp hv => mW_sq_lt_mZ_sq_of_gp_pos g gp v hgp hv
 200  ratio_eq_cos_sq  := fun g gp v hg hv => mW_over_mZ_sq_eq_cos_sq g gp v hg hv
 201  cos2_plus_sin2   := fun g gp hg => cos_sq_plus_sin_sq_thetaW g gp hg
 202  cos_sq_window    := fun g gp hg => cos_sq_thetaW_in_unit_interval g gp hg
 203

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.