English
To prove a property of a finite product, it suffices to show it is multiplicative and holds on factors.
Русский
Чтобы доказать свойство конечного произведения, достаточно показать его мультпликативность и верность для множителей.
LaTeX
$$$\\text{multiplicativity} \\; \\land \\; \\text{holds on each factor} \\Rightarrow \\text{property for finite product}$$$
Lean4
/-- To prove a property of a finite product, it suffices to prove that the property is
multiplicative and holds on factors. -/
@[to_additive /-- To prove a property of a finite sum, it suffices to prove that the property is
additive and holds on summands. -/
]
theorem finprod_mem_induction (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ x y, p x → p y → p (x * y))
(hp₂ : ∀ x ∈ s, p <| f x) : p (∏ᶠ i ∈ s, f i) :=
finprod_induction _ hp₀ hp₁ fun x => finprod_induction _ hp₀ hp₁ <| hp₂ x
