theorem proved term proof

`tenfold_equicardinal`

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

formal statement (Lean)

  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

proof body

Term-mode proof.

  65  rw [hA, hB]
  66
  67/-- 10 × 10 = 100. -/

depends on (4)

Lean names referenced from this declaration's body.

HasTenFold in IndisputableMonolith.CrossDomain.TenFoldCombinations decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use