pith. machine review for the scientific record. sign in
theorem proved term proof

tenfold_squared

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)

  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

proof body

Term-mode proof.

  72  unfold HasTenFold at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74
  75/-- 10 × D = 50. 50 is still below gap45+5. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.