coeff_isUnit — Mathlib

English

For a unit trinomial p, every coefficient on its support is a unit in Z, i.e., IsUnit(p.coeff k) for all k in supp(p).

Русский

Для единичного триномиала p каждый коэффициент на его опоре является единицей в Z, то есть IsUnit(p.coeff k) для всех k ∈ supp(p).

LaTeX

$$$\\forall k \\in p.\\mathrm{support},\\; IsUnit(p_{k})$$$

Lean4

theorem coeff_isUnit (hp : p.IsUnitTrinomial) {k : ℕ} (hk : k ∈ p.support) : IsUnit (p.coeff k) :=
  by
  obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
  have := support_trinomial' k m n (u : ℤ) v w hk
  rw [mem_insert, mem_insert, mem_singleton] at this
  rcases this with (rfl | rfl | rfl)
  · refine ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩
  · refine ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩
  · refine ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩

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