theorem proved term proof

`two_cube_pair_64`

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

formal statement (Lean)

  68theorem two_cube_pair_64
  69    {A B : Type} [Fintype A] [Fintype B]
  70    (hA : HasTwoCubeCount A) (hB : HasTwoCubeCount B) :
  71    Fintype.card (A × B) = 64 := by

proof body

Term-mode proof.

  72  unfold HasTwoCubeCount at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74
  75/-- Power set of a 2³-cube has size 2^8 = 256. -/

used by (1)

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

dft_q3_product in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
HasTwoCubeCount in IndisputableMonolith.CrossDomain.TwoCubeUniversality decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Power in IndisputableMonolith.Superhuman.Core decl_use