`tenFoldCombinationsCert`

definition

show as: view math explainer →

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

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

depends on

formal source

  88  squared_100 : ∀ (A B : Type) [Fintype A] [Fintype B],
  89    HasTenFold A → HasTenFold B → Fintype.card (A × B) = 100
  90
  91def tenFoldCombinationsCert : TenFoldCombinationsCert where
  92  finger_10 := finger_is_10
  93  digit_10 := digit_is_10
  94  lumSac_10 := lumSac_is_10
  95  dBlock_10 := dBlock_is_10
  96  ten_factoring := ten_eq_two_D
  97  ten_as_halves := ten_as_two_halves
  98  squared_100 := fun _ _ _ _ => tenfold_squared
  99
 100end IndisputableMonolith.CrossDomain.TenFoldCombinations

papers checked against this theorem

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