English
Given k < m and m < n with u ≠ 0 and w ≠ 0, the mirror of trinomial(k, m, n, u, v, w) equals trinomial(k, n - m + k, n, w, v, u).
Русский
Пусть k < m, m < n, u ≠ 0 и w ≠ 0. Тогда зеркальное отображение trinomial(k, m, n, u, v, w) равно trinomial(k, n - m + k, n, w, v, u).
LaTeX
$$$\\operatorname{mirror}\\left(\\operatorname{trinomial}(k,m,n,u,v,w)\\right) = \\operatorname{trinomial}\\left(k,\\; n - m + k,\\; n,\\; w,\\; v,\\; u\\right)$$$
Lean4
theorem trinomial_mirror (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hw : w ≠ 0) :
(trinomial k m n u v w).mirror = trinomial k (n - m + k) n w v u := by
rw [mirror, trinomial_natTrailingDegree hkm hmn hu, reverse, trinomial_natDegree hkm hmn hw, trinomial_def,
reflect_add, reflect_add, reflect_C_mul_X_pow, reflect_C_mul_X_pow, reflect_C_mul_X_pow,
revAt_le (hkm.trans hmn).le, revAt_le hmn.le, revAt_le le_rfl, add_mul, add_mul, mul_assoc, mul_assoc, mul_assoc, ←
pow_add, ← pow_add, ← pow_add, Nat.sub_add_cancel (hkm.trans hmn).le, Nat.sub_self, zero_add, add_comm,
add_comm (C u * X ^ n), ← add_assoc, ← trinomial_def]
