prod_iff — Mathlib

English

For a finite index set s and a function f : ι → M into a commutative monoid M, the product ∏ a ∈ s f a is a unit iff every factor f a is a unit.

Русский

Для конечного множества индексов s и функции f: ι → M в коммутативном моноиде M произведение ∏ a ∈ s f a является единичным элементом тогда и только тогда, когда каждый фактор f a является единичным элементом.

LaTeX

$$$$ \\text{IsUnit}\\left(\\prod_{a \\in s} f(a)\\right) \\iff \\forall a \\in s, \\text{IsUnit}(f(a)). $$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_iff [CommMonoid M] {f : ι → M} : IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a) := by
  induction s using Finset.cons_induction with grind

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