prod_eq_one

Mathlib.Data.Fintype.BigOperators

URI: https://scilib.ai/kg/mathlib#Fintype.prod_eq_one

English

If every value f(a) equals 1 for all a, then the product over a is 1.

Русский

Если для всех a выполняется f(a)=1, то произведение по всем a равно 1.

LaTeX

$$$\\prod_{a \\in \\mathrm{univ}} f(a) = 1$$$

Lean4

@[to_additive]
theorem prod_eq_one (f : α → M) (h : ∀ a, f a = 1) : ∏ a, f a = 1 :=
  Finset.prod_eq_one fun a _ha => h a

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

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

Разделы

Аффилиация

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