finMulAntidiag_three — Mathlib

English

For a fixed n and a function a from Fin 3 to Nat that lies in finMulAntidiag 3 n, the product a(0) · a(1) · a(2) equals n.

Русский

Для фиксированного n и функции a : Fin 3 → Nat, если a ∈ finMulAntidiag 3 n, тогда a(0)·a(1)·a(2)=n.

LaTeX

$$$a:\ Fin 3 \to \mathbb{N},\; a\in\text{finMulAntidiag}(3,n) \Rightarrow a(0)\,a(1)\,a(2)=n$$$

Lean4

theorem finMulAntidiag_three {n : ℕ} (a) (ha : a ∈ finMulAntidiag 3 n) : a 0 * a 1 * a 2 = n := by
  rw [← (mem_finMulAntidiag.mp ha).1, Fin.prod_univ_three a]

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