English
For any L and i with i < length(L), the product of the tail after removing the element at position i+1 equals the inverse of the i-th element times the product of the tail after removing i.
Русский
Для списка L и индекса i, где i < длина(L), произведение хвоста после удаления элемента на позиции i+1 равно обратному i-го элемента, умноженному на произведение хвоста после удаления i.
LaTeX
$$$\forall (L : List G) (i : \mathbb{N}) (p : i < L.length), (L.drop (i + 1)).prod = L[i]^{-1} * (L.drop i).prod$$
Lean4
/-- Counterpart to `List.prod_take_succ` when we have an inverse operation -/
@[to_additive (attr := simp) /-- Counterpart to `List.sum_take_succ` when we have a negation operation -/
]
theorem prod_drop_succ : ∀ (L : List G) (i : ℕ) (p : i < L.length), (L.drop (i + 1)).prod = L[i]⁻¹ * (L.drop i).prod
| [], _, p => False.elim (Nat.not_lt_zero _ p)
| _ :: _, 0, _ => by simp
| _ :: xs, i + 1, p => prod_drop_succ xs i (Nat.lt_of_succ_lt_succ p)
