  15
  16namespace IndisputableMonolith.Anthropology.KinshipStructuresFromConfigDim
  17
  18inductive KinshipSystem where
  19  | hawaiian
  20  | eskimo
  21  | iroquois
  22  | sudanese
  23  | omaha
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem kinshipSystem_count : Fintype.card KinshipSystem = 5 := by decide
  27
  28structure KinshipStructureCert where
  29  five_systems : Fintype.card KinshipSystem = 5
  30
  31def kinshipStructureCert : KinshipStructureCert where
  32  five_systems := kinshipSystem_count
  33
  34end IndisputableMonolith.Anthropology.KinshipStructuresFromConfigDim

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.