prod_univ_two' — Mathlib

English

For any f: ι → M and a,b ∈ ι, the product over Fin 2 of f(![a,b] i) equals f(a) f(b).

Русский

Для любого f: ι → M и элементoв a,b ∈ ι произведение по Fin 2 от функции, записанной через двухэлементный вектор [a,b], равно f(a) f(b).

LaTeX

$$$\displaystyle \prod_{i \in \mathrm{Fin}(2)} f(!(a,b) \, i) = f(a) \cdot f(b).$$$

Lean4

@[to_additive]
theorem prod_univ_two' (f : ι → M) (a b : ι) : ∏ i, f (![a, b] i) = f a * f b :=
  prod_univ_two _

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