pith. machine review for the scientific record. sign in
structure definition def or abbrev

TwoCubeUniversalityCert

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)

  99structure TwoCubeUniversalityCert where
 100  dft_is_2cube : HasTwoCubeCount DFTMode
 101  q3_is_2cube : HasTwoCubeCount Q3Vertex
 102  pauli_is_2cube : HasTwoCubeCount PauliElement
 103  tick_is_2cube : HasTwoCubeCount TickPhase
 104  all_equicardinal : ∀ (A B : Type) [Fintype A] [Fintype B],
 105    HasTwoCubeCount A → HasTwoCubeCount B →
 106    Fintype.card A = Fintype.card B
 107  pair_64 : Fintype.card (DFTMode × Q3Vertex) = 64
 108  sixtyfour_identities : 64 = 8 * 8 ∧ 64 = 2^6
 109

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.