English
Let M be a commutative monoid. Let s be a nonempty finite set of indices and f: ι → M. If p is closed under multiplication, holds at 1, and p(f(x)) holds for every x ∈ s, then p(∏_{x ∈ s} f(x)).
Русский
Пусть M — коммутативный моноид. Пусть s — непустое конечное подмножество ι и f: ι → M. Если p замкнуто относительно умножения, p(1) истинно, и p(f(x)) верно для каждого x ∈ s, то p(∏_{x ∈ s} f(x)).
LaTeX
$$$$\forall s: \mathrm{Finset}(\iota)\; s.\mathrm{Nonempty} \Rightarrow \forall f: \iota \to M\; \forall p: M \to \mathrm{Prop},\; (\forall a\, b:\! M,\; p(a) \to p(b) \to p(a b)) \land (\forall x \in s, p(f(x))) \Rightarrow p\left(\prod_{x \in s} f(x)\right).$$$$
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_nonempty {M : Type*} [CommMonoid M] (f : ι → M) (p : M → Prop)
(hom : ∀ a b, p a → p b → p (a * b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p <| f x) : p <| ∏ x ∈ s, f x :=
Multiset.prod_induction_nonempty p hom (by simp [nonempty_iff_ne_empty.mp nonempty])
(Multiset.forall_mem_map_iff.mpr base)
