prod_induction — Mathlib

English

For a list l of a monoid M, to prove a property P of l.prod it suffices to show P is closed under multiplication, P 1 holds, and P holds for each element of l.

Русский

Для списка l моноида M доказательство свойства P о l.prod достаточно, если P сохраняется под умножением, верно для 1, и выполняется для каждого элемента списка.

LaTeX

$$$\text{prod_induction}(f, p, \text{hom}, \text{unit}, \text{base})$$$

Lean4

@[to_additive]
theorem prod_induction (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ l, p x) :
    p l.prod := by
  induction l with
  | nil => simpa
  | cons a l ih =>
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)

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