theorem
proved
ckm_params_3_plus_1
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 236.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
233def ckmParameters : ℕ := 4
234
235/-- 4 = 3 + 1 (angles + CP phase). -/
236theorem ckm_params_3_plus_1 : ckmParameters = 3 + 1 := rfl
237
238end
239
240end WeakForceEmergence
241end Physics
242end IndisputableMonolith