finprod_eq_one_of_forall_eq_one

Mathlib.Algebra.BigOperators.Finprod

URI: https://scilib.ai/kg/mathlib#finprod_eq_one_of_forall_eq_one

English

If f(x)=1 for all x, then the finprod over α of f equals 1.

Русский

Если для всех x выполняется f(x)=1, то $ \\prodᶠ i, f(i) = 1 $.

LaTeX

$$$\\displaystyle (\\forall x, f(x)=1) \\Rightarrow \\prod\\ᶠ i, f(i) = 1$$$

Lean4

@[to_additive]
theorem finprod_eq_one_of_forall_eq_one {f : α → M} (h : ∀ x, f x = 1) : ∏ᶠ i, f i = 1 := by simp +contextual [h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru