English
If L is cyclically reduced, then flattening n copies of L preserves cyclically reduced property.
Русский
Если L циклически сокращено, то свертка n копий L сохраняет это свойство.
LaTeX
$$$$ \\forall n:\\mathbb{N},\\ \\mathrm{IsCyclicallyReduced}(\\mathrm{List.flatten}(\\mathrm{List.replicate}\\ n\\ L)) $$ given \\mathrm{IsCyclicallyReduced}(L). $$$$
Lean4
@[to_additive]
theorem flatten_replicate (n : ℕ) (h : IsCyclicallyReduced L) : IsCyclicallyReduced (List.replicate n L).flatten := by
match n, L with
| 0, _ => simp
| n + 1, [] => simp
| n + 1,
(head :: tail) =>
rw [isCyclicallyReduced_iff, IsReduced, List.isChain_flatten (by simp)]
refine ⟨⟨by simpa [IsReduced] using h.isReduced, List.isChain_replicate_of_rel _ h.2⟩, fun _ ha _ hb ↦ ?_⟩
rw [Option.mem_def, List.getLast?_flatten_replicate (h := by simp +arith)] at ha
rw [Option.mem_def, List.head?_flatten_replicate (h := by simp +arith)] at hb
exact h.2 _ ha _ hb
