DBlockElement

formal source

  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
  67/-- 10 × 10 = 100. -/
  68theorem tenfold_squared
  69    {A B : Type} [Fintype A] [Fintype B]
  70    (hA : HasTenFold A) (hB : HasTenFold B) :
  71    Fintype.card (A × B) = 100 := by
  72  unfold HasTenFold at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74