def definition def or abbrev

`sin2_theta_W`

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

formal statement (Lean)

  47noncomputable def sin2_theta_W : ℝ := (3 - Constants.phi) / 6

Definition body.

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

BosonVerificationCert in IndisputableMonolith.Masses.BosonVerification decl_use
cos2_theta_W in IndisputableMonolith.Masses.BosonVerification decl_use
sin2_theta_W_bounds in IndisputableMonolith.Masses.BosonVerification decl_use
wz_ratio_eq_cos2 in IndisputableMonolith.Masses.BosonVerification decl_use
cos_theta_W in IndisputableMonolith.Physics.ElectroweakBosons decl_use
sin2_theta_approx in IndisputableMonolith.Physics.ElectroweakBosons decl_use
sin2_theta_not_half in IndisputableMonolith.Physics.ElectroweakBosons decl_use
sin2_theta_W in IndisputableMonolith.Physics.ElectroweakBosons decl_use
sin2_theta_window in IndisputableMonolith.Physics.ElectroweakBosons decl_use
wz_ratio_equals_cos_theta in IndisputableMonolith.Physics.ElectroweakBosons decl_use

Lean names referenced from this declaration's body.