English
Dropping the first i elements of p yields the tail of p starting at i, of length p.length - i, with indices shifted by i.
Русский
Удаление первых i элементов p даёт хвост p, начинающийся с i, длиной p.length − i, с приращением индексов на i.
LaTeX
$$$$ \\operatorname{length}(p) - i \\quad \\text{and} \\quad (p^{(i)})_j = p_{j+i} \\text{ for appropriate } j. $$$$
Lean4
/-- Given the series `a₀ -r→ … -r→ aᵢ -r→ … -r→ aₙ`, the series `aᵢ₊₁ -r→ … -r→ aₙ`. -/
@[simps! length]
def drop (p : RelSeries r) (i : Fin (p.length + 1)) : RelSeries r
where
length := p.length - i
toFun := fun ⟨j, h⟩ => p.toFun ⟨j + i, by omega⟩
step := fun ⟨j, h⟩ => by
convert p.step ⟨j + i.1, by omega⟩
simp only [Fin.succ_mk]; omega
