prod_univ_iff — Mathlib

English

If ι is finite, for any f: ι → M into a commutative monoid M, IsUnit (∏ a, f a) holds iff every f a is a unit.

Русский

Пусть ι конечен; для любой функции f: ι → M в коммутативном моноиде M единичность произведения ∏ a f(a) эквивалентна единичности каждого f(a).

LaTeX

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

Lean4

@[to_additive]
theorem prod_univ_iff [Fintype ι] [CommMonoid M] {f : ι → M} : IsUnit (∏ a, f a) ↔ ∀ a, IsUnit (f a) := by simp

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