`DecimalDigit`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.TenFoldCombinations
domain: CrossDomain
line: 36 · 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 36.

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

  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
  62    {A B : Type} [Fintype A] [Fintype B]
  63    (hA : HasTenFold A) (hB : HasTenFold B) :
  64    Fintype.card A = Fintype.card B := by
  65  rw [hA, hB]
  66

papers checked against this theorem

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