pith. machine review for the scientific record. sign in
def 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)

 110def twoCubeUniversalityCert : TwoCubeUniversalityCert where
 111  dft_is_2cube := dft_has_2cube

proof body

Definition body.

 112  q3_is_2cube := q3_has_2cube
 113  pauli_is_2cube := pauli_has_2cube
 114  tick_is_2cube := tick_has_2cube
 115  all_equicardinal := fun _ _ _ _ => two_cube_equicardinal
 116  pair_64 := dft_q3_product
 117  sixtyfour_identities := sixtyfour_identities
 118
 119end IndisputableMonolith.CrossDomain.TwoCubeUniversality

depends on (8)

Lean names referenced from this declaration's body.