coe_prod — Mathlib

English

For a finite set s and a family of units f(i) ∈ M, the product of the units, regarded as elements of M, equals the product of their underlying values in M.

Русский

Для конечного множества s и семейства единиц f(i) ∈ M произведение единиц, рассматриваемое как элементы M, равно произведению самих значений в M.

LaTeX

$$$\big(\prod i \in s, f(i)\big)^{\mathrm{val}} = \prod i \in s, (f(i))^{\mathrm{val}}$$$

Lean4

@[simp, norm_cast]
theorem coe_prod [CommMonoid M] (f : α → Mˣ) (s : Finset α) : (↑(∏ i ∈ s, f i) : M) = ∏ i ∈ s, (f i : M) :=
  map_prod (Units.coeHom M) _ _

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