baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-15 16:14:48 +01:00
parent 94e65475a3
commit 141c4ba029
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/thue_morse2.v
View File

@ -1,7 +1,7 @@
(** * The Thue-Morse sequence (part 2)
The following lemmas and theorems are all related to
squares of odd length in the Thue-Morse sequence.
squares and cubes in the Thue-Morse sequence.
Proofs in this file are long; many parts are repeated
from copy/paste operations. Many ad-hoc lemmas could
@ -9,6 +9,7 @@
But some powerful theorems are provided here:
- tm_step_cubefree (there is no cube in the sequence)
- tm_step_square_size (all squared factors of odd
length have length 1 or 3).
*)