def definition def or abbrev

`ckmlambdaCert`

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

formal statement (Lean)

  73noncomputable def ckmlambdaCert : CKMLambdaCert where
  74  wolfenstein_A := wolfensteinA_val

proof body

Definition body.

  75  A_in_pdg := wolfensteinA_in_pdg_band
  76  cabibbo_phi3 := phi3_eq
  77  cabibbo_band := cabibbo_in_band
  78
  79end IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder

depends on (6)

Lean names referenced from this declaration's body.

cabibbo_in_band in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder decl_use
CKMLambdaCert in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder decl_use
phi3_eq in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder decl_use
wolfensteinA_in_pdg_band in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder decl_use
wolfensteinA_val in IndisputableMonolith.Foundation.CKMLambdaFromPhiLadder decl_use
wolfenstein_A in IndisputableMonolith.StandardModel.CKMMatrix decl_use