theorem proved term proof

`pair_product_25`

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

formal statement (Lean)

  68theorem pair_product_25
  69    {A B : Type} [Fintype A] [Fintype B]
  70    (hA : HasConfigDim5 A) (hB : HasConfigDim5 B) :
  71    Fintype.card (A × B) = 25 := by

proof body

Term-mode proof.

  72  unfold HasConfigDim5 at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74
  75/-- Two D=5 types are equicardinal (trivially, both = 5). -/

depends on (4)

Lean names referenced from this declaration's body.

HasConfigDim5 in IndisputableMonolith.CrossDomain.ConfigDimUniversality decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use