theorem proved term proof

`configDim5_equicardinal`

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

formal statement (Lean)

  76theorem configDim5_equicardinal
  77    {A B : Type} [Fintype A] [Fintype B]
  78    (hA : HasConfigDim5 A) (hB : HasConfigDim5 B) :
  79    Fintype.card A = Fintype.card B := by

proof body

Term-mode proof.

  80  rw [hA, hB]
  81
  82/-- Concrete instance: sensory × emotion × biological = 125. -/

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