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)
57noncomputable def wolfenstein_A : ℝ := 0.82
proof body
Definition body.
58
59/-- The Wolfenstein parameter ρ ≈ 0.14. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ckmlambdaCert
in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder
decl_use
-
CKMLambdaCert
in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder
decl_use
-
V_cb
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