theorem
proved
digit_is_10
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.TenFoldCombinations on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
75/-- 10 × D = 50. 50 is still below gap45+5. -/
76theorem tenfold_times_D : (10 : ℕ) * 5 = 50 := by decide
77
78/-- Two 5-fold halves of a 10-fold: decimal = 2 × 5 (half-halves). -/
79theorem ten_as_two_halves : (10 : ℕ) = 5 + 5 := by decide
80