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)
54noncomputable def wolfenstein_lambda : ℝ := cabibboAngle
proof body
Definition body.
55
56/-- The Wolfenstein parameter A ≈ 0.82. -/
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
-
V_cb
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_cd
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_cs
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_td
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_ts
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_ub
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_ud
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_us
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
cabibboAngle
in IndisputableMonolith.Physics.ThreeGenerations
decl_use
-
cabibboAngle
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use