prod_isUnit — Mathlib

English

If every element of a list L in a monoid M is a unit, then the product L.prod is a unit.

Русский

Если каждый элемент списка L в моноиде M является единичным элементом, то произведение L.prod также единично.

LaTeX

$$∀{L}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod$$

Lean4

@[to_additive]
theorem prod_isUnit : ∀ {L : List M}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod
  | [], _ => by simp
  | h :: t, u => by
    simp only [List.prod_cons]
    exact IsUnit.mul (u h mem_cons_self) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))

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