`Finger`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.TenFoldCombinations
domain: CrossDomain
line: 31 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.TenFoldCombinations on GitHub at line 31.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  28/-- A type has 10-fold structure iff |T| = 10 = 2·5. -/
  29def HasTenFold (T : Type) [Fintype T] : Prop := Fintype.card T = 10
  30
  31inductive Finger where
  32  | thumbL | indexL | middleL | ringL | pinkyL
  33  | thumbR | indexR | middleR | ringR | pinkyR
  34  deriving DecidableEq, Repr, BEq, Fintype
  35
  36inductive DecimalDigit where
  37  | d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9
  38  deriving DecidableEq, Repr, BEq, Fintype
  39
  40inductive LumbarSacralVert where
  41  | l1 | l2 | l3 | l4 | l5 | s1 | s2 | s3 | s4 | s5
  42  deriving DecidableEq, Repr, BEq, Fintype
  43
  44inductive DBlockElement where
  45  | sc | ti | v | cr | mn | fe | co | ni | cu | zn  -- first d-block period
  46  deriving DecidableEq, Repr, BEq, Fintype
  47
  48theorem finger_is_10 : HasTenFold Finger := by
  49  unfold HasTenFold; decide
  50theorem digit_is_10 : HasTenFold DecimalDigit := by
  51  unfold HasTenFold; decide
  52theorem lumSac_is_10 : HasTenFold LumbarSacralVert := by
  53  unfold HasTenFold; decide
  54theorem dBlock_is_10 : HasTenFold DBlockElement := by
  55  unfold HasTenFold; decide
  56
  57/-- 10 = 2 · 5 factorisation. -/
  58theorem ten_eq_two_D : (10 : ℕ) = 2 * 5 := by decide
  59
  60/-- Two 10-folds have the same cardinality. -/
  61theorem tenfold_equicardinal

papers checked against this theorem

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