cast_prod — Mathlib

English

Equivalent restatement: for a finite index set, the cast distributes over products: (s.prod fun i => f i).cast = s.prod fun i => (f i).cast.

Русский

Эквивалентное утверждение: для конечного множества индексов распределять по произведениям: (∏ i∈s f i) cast = ∏ i∈s (f i cast).

LaTeX

$$$\left(\prod_{i\in s} f(i)\right)^{\uparrow} = \prod_{i\in s} f(i)^{\uparrow}$$$

Lean4

@[simp, norm_cast]
theorem cast_prod {R : Type*} [CommRing R] (f : ι → ℤ) (s : Finset ι) : (↑(∏ i ∈ s, f i) : R) = ∏ i ∈ s, (f i : R) :=
  map_prod (Int.castRingHom R) _ _

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