structure
definition
ConstitutionalFormsCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Governance.ConstitutionalFormsFromConfigDim on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25
26theorem constitutionalForm_count : Fintype.card ConstitutionalForm = 5 := by decide
27
28structure ConstitutionalFormsCert where
29 five_forms : Fintype.card ConstitutionalForm = 5
30
31def constitutionalFormsCert : ConstitutionalFormsCert where
32 five_forms := constitutionalForm_count
33
34end IndisputableMonolith.Governance.ConstitutionalFormsFromConfigDim