headI_mul_tail_prod_of_ne_nil — Mathlib

English

If L is nonempty, then L.headI * L.tail.prod = L.prod.

Русский

Если список непустой, то произведение головы и хвоста равно произведению всего списка.

LaTeX

$$[Inhabited] l ≠ ∅ → l.headI * l.tail.prod = l.prod$$

Lean4

/-- Same as `get?_zero_mul_tail_prod`, but avoiding the `List.headI` garbage complication by
  requiring the list to be nonempty. -/
@[to_additive /-- Same as `get?_zero_add_tail_sum`, but avoiding the `List.headI` garbage
      complication by requiring the list to be nonempty. -/
    ]
theorem headI_mul_tail_prod_of_ne_nil [Inhabited M] (l : List M) (h : l ≠ []) : l.headI * l.tail.prod = l.prod := by
  cases l <;> [contradiction; simp]

Похожие утверждения