IsUnitTrinomial — Mathlib

English

A unit trinomial is a trinomial whose coefficients are units. Formally, there exist k, m, n with k < m and m < n, and u, v, w which are units in Z, such that p = trinomial k m n (u : Z) v w.

Русский

Единичный триномиал — это триномиал, коэффициенты которого — единичные элементы. Формально существует k < m < n и u, v, w ∈ Units ℤ такие, что p = trinomial k m n (u : ℤ) v w.

LaTeX

$$$\\exists k,m,n \\in \\mathbb{N},\\ k < m \\land m < n \\land u,v,w \\in \\mathbb{Z}^{\\times},\\ p = \\mathrm{trinomial}(k,m,n\\,(u:\\mathbb{Z})\\,v\\,w)$$$

Lean4

/-- A unit trinomial is a trinomial with unit coefficients. -/
def IsUnitTrinomial :=
  ∃ (k m n : ℕ) (_ : k < m) (_ : m < n) (u v w : Units ℤ), p = trinomial k m n (u : ℤ) v w

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