English
If m ∈ FP a, there exists n such that for all m' ∈ FP(a.drop n), m * m' ∈ FP a.
Русский
Если m ∈ FP(a), существует n, что для всех m' ∈ FP(a.drop n) выполняется m * m' ∈ FP a.
LaTeX
$$For hm ∈ FP(a), ∃ n, ∀ m' ∈ FP(a.drop n), m * m' ∈ FP a.$$
Lean4
/-- If `m` and `m'` are finite products in `M`, then so is `m * m'`, provided that `m'` is obtained
from a subsequence of `M` starting sufficiently late. -/
@[to_additive /-- If `m` and `m'` are finite sums in `M`, then so is `m + m'`, provided that `m'`
is obtained from a subsequence of `M` starting sufficiently late. -/
]
theorem mul {M} [Semigroup M] {a : Stream' M} {m : M} (hm : m ∈ FP a) : ∃ n, ∀ m' ∈ FP (a.drop n), m * m' ∈ FP a := by
induction hm with
| head' a => exact ⟨1, fun m hm => FP.cons a m hm⟩
| tail' a m _ ih =>
obtain ⟨n, hn⟩ := ih
use n + 1
intro m' hm'
exact FP.tail _ _ (hn _ hm')
| cons' a m _ ih =>
obtain ⟨n, hn⟩ := ih
use n + 1
intro m' hm'
rw [mul_assoc]
exact FP.cons _ _ (hn _ hm')
