def
definition
electrowealCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ElectrowealUnificationFromRS on GitHub at line 43.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
40 five_observables : Fintype.card EWObservable = 5
41 rank_sum : rankEW = rankSU2 + rankU1
42
43def electrowealCert : ElectroweakCert where
44 ew_rank_D := rankEW_eq_D
45 five_observables := ewObservableCount
46 rank_sum := ew_from_su2_u1
47
48end IndisputableMonolith.Physics.ElectrowealUnificationFromRS