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)
53def mZ_sq (g gp v : ℝ) : ℝ := (g ^ 2 + gp ^ 2) * v ^ 2 / 4
proof body
Definition body.
54
55/-- W boson mass: `m_W = g v / 2` (for `g, v > 0`). -/
used by (9)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ElectroweakMassBridgeCert
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mW_over_mZ_eq_cos_thetaW
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mW_over_mZ_sq
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mW_over_mZ_sq_eq_cos_sq
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mW_sq_le_mZ_sq
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mW_sq_lt_mZ_sq_of_gp_pos
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mZ
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mZ_sq_ge_mW_sq
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
-
mZ_sq_nonneg
in IndisputableMonolith.StandardModel.ElectroweakMassBridge
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
W
in IndisputableMonolith.Masses.Anchor
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use
-
m_W
in IndisputableMonolith.StandardModel.WZMassRatio
decl_use