pith. machine review for the scientific record. sign in
def definition def or abbrev

tenFoldCombinationsCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  91def tenFoldCombinationsCert : TenFoldCombinationsCert where
  92  finger_10 := finger_is_10

proof body

Definition body.

  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

depends on (8)

Lean names referenced from this declaration's body.