def
definition
smLagrangianCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.StandardModelLagrangianStructure on GitHub at line 45.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
42 main4_2sq : mainTermCount = 2 ^ 2
43 total5 : totalTermCount = mainTermCount + 1
44
45def smLagrangianCert : SMLagrangianCert where
46 five_sectors := smSectorCount
47 main4_2sq := mainTerms_2sq
48 total5 := total_terms
49
50end IndisputableMonolith.Physics.StandardModelLagrangianStructure