def
definition
grayCover3
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Patterns.GrayCycle on GitHub at line 212.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
209theorem grayCycle3_period : (2 ^ 3) = 8 := by decide
210
211/-- The 3-bit Gray cycle can be viewed as a GrayCover of period 8. -/
212def grayCover3 : GrayCover 3 8 :=
213{ path := grayCycle3Path
214, complete := grayCycle3_surjective
215, oneBit_step := grayCycle3_oneBit_step
216}
217
218end Patterns
219end IndisputableMonolith