def definition def or abbrev

`vev`

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

formal statement (Lean)

  60noncomputable def vev : ℝ := 246

Definition body.

  61
  62/-- W-boson observed mass in GeV. -/

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

higgs_mechanism_nonzero_vev in IndisputableMonolith.QFT.HiggsMechanism decl_use
higgs_mechanism_vev_ne_one in IndisputableMonolith.QFT.HiggsMechanism decl_use
massParameter in IndisputableMonolith.QFT.HiggsMechanism decl_use
mass_parameter_pos in IndisputableMonolith.QFT.HiggsMechanism decl_use
particleMass in IndisputableMonolith.QFT.HiggsMechanism decl_use
symmetry_broken in IndisputableMonolith.QFT.HiggsMechanism decl_use
vev in IndisputableMonolith.QFT.HiggsMechanism decl_use
vev_gt_one in IndisputableMonolith.QFT.HiggsMechanism decl_use
vev_pos in IndisputableMonolith.QFT.HiggsMechanism decl_use
wBosonMass in IndisputableMonolith.QFT.HiggsMechanism decl_use
zBosonMass in IndisputableMonolith.QFT.HiggsMechanism decl_use
vev in IndisputableMonolith.StandardModel.ElectroweakBreaking decl_use
mH_naive in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_prediction_in_interval in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level2 in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level2_in_range in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level3 in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
mH_rs_level3_pos in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use
vev_pos in IndisputableMonolith.StandardModel.HiggsRungAssignment decl_use

Lean names referenced from this declaration's body.

W in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use
vev in IndisputableMonolith.QFT.HiggsMechanism decl_use
vev in IndisputableMonolith.StandardModel.ElectroweakBreaking decl_use