prod_eq_one_iff_of_one_le

Mathlib.Algebra.Order.BigOperators.Group.Finset

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

← MathLib Explorer

English

If f ≤ 1, then ∏ i f(i) = 1 iff f ≡ 1 (the constant function 1).

Русский

Если f ≤ 1, то произведение равно 1 тогда и только тогда, когда f ≡ 1.

LaTeX

$$$f \le 1 \Rightarrow \left( \prod_{i} f(i) = 1 \iff f = 1 \right)$$$

Lean4

@[to_additive]
theorem prod_eq_one_iff_of_one_le (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
  (Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans <| by simp [funext_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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