Theorems · Theorem · field theory

Polynomial.trinomial_mirror

∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → u ≠ 0 → w ≠ 0 → (Polynomial.trinomial k m n u v w).mirror = Polynomial.trinomial k (n - m + k) n w v u

Defined in

Mathlib.Algebra.Polynomial.UnitTrinomial

Cited by

4 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring