def definition def or abbrev

`grayCycle3`

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

formal statement (Lean)

 203def grayCycle3 : GrayCycle 3 :=

Definition body.

 204{ path := grayCycle3Path
 205, inj := grayCycle3_injective
 206, oneBit_step := grayCycle3_oneBit_step
 207}
 208

Lean names referenced from this declaration's body.