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)
74noncomputable def V_us : ℂ := wolfenstein_lambda
used by (15)
From the project-wide theorem graph. These declarations reference this one in their body.
-
torsion_differences
in IndisputableMonolith.Particles.CKMDerivation
decl_use
-
jarlskog_witness_pos
in IndisputableMonolith.Physics.CKM
decl_use
-
s12_w
in IndisputableMonolith.Physics.CKM
decl_use
-
V_cd
in IndisputableMonolith.Physics.CKM
decl_use
-
V_ud
in IndisputableMonolith.Physics.CKM
decl_use
-
V_us
in IndisputableMonolith.Physics.CKM
decl_use
-
phi_inv3_upper_bound
in IndisputableMonolith.Physics.CKMGeometry
decl_use
-
V_cb_pred
in IndisputableMonolith.Physics.CKMGeometry
decl_use
-
V_ub_match
in IndisputableMonolith.Physics.CKMGeometry
decl_use
-
mk_toList
in IndisputableMonolith.RecogSpec.ObservablePayloads
decl_use
-
canonical_V_ub
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
canonical_V_us
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
V_ub_from_bridge
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
experimentalValues
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
unitarity_triangle_valid
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
V_us
in IndisputableMonolith.Physics.CKM
decl_use
-
wolfenstein_lambda
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use