isSquare_prod — Mathlib

English

If every factor f_i is a square in a commutative monoid, then their finite product is also a square.

Русский

Если каждый фактор f_i является квадратом в коммутативном моноиде, тогда их конечное произведение тоже является квадратом.

LaTeX

$$$\\text{IsSquare}\\left(\\prod_{i \\in s} f_i\\right).$$$

Lean4

@[to_additive]
theorem isSquare_prod {s : Finset ι} (f : ι → M) (h : ∀ c ∈ s, IsSquare (f c)) : IsSquare (∏ i ∈ s, f i) :=
  by
  rw [isSquare_iff_exists_sq]
  use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)
  rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]
  congr
  ext i
  rw [← @sq]
  exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

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