prod_eq_of_mem_finMulAntidiag

Mathlib.Algebra.Order.Antidiag.Nat

URI: https://scilib.ai/kg/mathlib#Nat.prod_eq_of_mem_finMulAntidiag

English

If f ∈ finMulAntidiag d n, then the product over i of f(i) equals n.

Русский

Если f ∈ finMulAntidiag d n, то произведение по i f(i) равно n.

LaTeX

$$$f\in\text{finMulAntidiag}(d,n)\Rightarrow \prod_i f(i)=n$$$

Lean4

theorem prod_eq_of_mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} (hf : f ∈ finMulAntidiag d n) : ∏ i, f i = n :=
  (mem_finMulAntidiag.mp hf).1

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

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

Разделы

Аффилиация

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