English
To prove a property P of a finite product, it suffices to show P is multiplicative, holds at the unit element 1, and holds on each factor; then P holds for the product over s.
Русский
Чтобы доказать свойство P для произведения элементов, достаточно показать, что свойство мультпликативное, выполняется на единице 1 и на каждом множителе; тогда P выполняется для произведения элементов множества.
LaTeX
$$$\text{ProdInduction}(f, p, \text{hom}, \text{unit}, \text{base})$$$
Lean4
/-- To prove a property of a product, it suffices to prove that
the property is multiplicative and holds on factors. -/
@[to_additive /-- To prove a property of a sum, it suffices to prove that
the property is additive and holds on summands. -/
]
theorem prod_induction {M : Type*} [CommMonoid M] (f : ι → M) (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b))
(unit : p 1) (base : ∀ x ∈ s, p <| f x) : p <| ∏ x ∈ s, f x :=
Multiset.prod_induction _ _ hom unit (Multiset.forall_mem_map_iff.mpr base)
