prod_induction — Mathlib

English

For any commutative monoid M, given a predicate p with p(a) closed under multiplication and containing 1, and containing all elements of s, then p(s.prod).

Русский

Для коммутативного моноида M, если тождественность p(a) сохраняется при умножении и выполняется для единицы, и p истинно для всех элементов s, то p истинно для s.prod.

LaTeX

$$$\\forall p\\,(s: Multiset M),\\; (\\forall a b, p a \\to p b \\to p (a \\cdot b)) \\to p 1 \\to (\\forall a \\in s, p a) \\to p \\; s.\\mathrm{prod}$$$

Lean4

@[to_additive]
theorem prod_induction (p : M → Prop) (s : Multiset M) (p_mul : ∀ a b, p a → p b → p (a * b)) (p_one : p 1)
    (p_s : ∀ a ∈ s, p a) : p s.prod := by
  rw [prod_eq_foldr]
  exact foldr_induction (· * ·) 1 p s p_mul p_one p_s

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