pith. machine review for the scientific record. sign in
structure definition def or abbrev

ConfigDimUniversalityCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 101structure ConfigDimUniversalityCert where
 102  sensory_5 : HasConfigDim5 SensoryModality
 103  emotion_5 : HasConfigDim5 PrimaryEmotion
 104  biological_5 : HasConfigDim5 BiologicalState
 105  economic_5 : HasConfigDim5 EconomicCycle
 106  linguistic_5 : HasConfigDim5 LinguisticRole
 107  triple_125 : ∀ (A B C : Type) [Fintype A] [Fintype B] [Fintype C],
 108    HasConfigDim5 A → HasConfigDim5 B → HasConfigDim5 C →
 109    Fintype.card (A × B × C) = 125
 110  five_domain_3125 :
 111    Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState ×
 112                  EconomicCycle × LinguisticRole) = 3125
 113  five_pow_five : (5 : ℕ)^5 = 3125
 114

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.