module module

`IndisputableMonolith.Physics.CKMElementScoreCard`

show as: view Lean formalization →

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

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.CKMGeometry module_import
IndisputableMonolith.Physics.MixingDerivation module_import

declarations in this module (8)

theorem row_V_us L33
theorem row_V_cb L35
theorem row_V_ub L37
theorem row_vus_eq_geometry L39
theorem row_vcb_eq_geometry L42
theorem row_vub_eq_leakage L44
structure CKMElementScoreCardCert L46
theorem ckmElementScoreCardCert_holds L54