def
definition
topologicalChargesCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.TopologicalChargesFromConfigDim on GitHub at line 30.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
27structure TopologicalChargesCert where
28 five_charges : Fintype.card TopologicalCharge = 5
29
30def topologicalChargesCert : TopologicalChargesCert where
31 five_charges := topologicalCharge_count
32
33end IndisputableMonolith.Physics.TopologicalChargesFromConfigDim