English
A technical intermediate identity expressing a relation between the coefficients of p = trinomial k m n (u) v w and the filtered representation of p*m/p.mirror.
Русский
Техническое промежуточное тождество, выражающее отношение коэффициентов p = trinomial k m n (u) v w и отфильтрованного представления p*m/p.mirror.
LaTeX
$$$C(v) * (C(u) * X^{m+n} + C(w) * X^{n - m + k + n}) = \\langle Finsupp.filter (\\cdot \\in Set.Ioo (k+n) (n+n)) (p * p.mirror).toFinsupp \\rangle$$$
Lean4
theorem irreducible_aux1 {k m n : ℕ} (hkm : k < m) (hmn : m < n) (u v w : Units ℤ)
(hp : p = trinomial k m n (u : ℤ) v w) :
C (v : ℤ) * (C (u : ℤ) * X ^ (m + n) + C (w : ℤ) * X ^ (n - m + k + n)) =
⟨Finsupp.filter (· ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp⟩ :=
by
have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le]
rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero]
simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial, toFinsupp_add,
toFinsupp_monomial, AddMonoidAlgebra, Finsupp.filter_add]
rw [Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg,
Finsupp.filter_single_of_neg, Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos,
Finsupp.filter_single_of_neg, Finsupp.filter_single_of_pos, Finsupp.filter_single_of_neg]
· simp only [add_zero, zero_add]
-- Porting note: the next `rw` is needed to see through the defeq `Finsupp = AddMonoidAlgebra`
rw [ofFinsupp_add]
simp only [ofFinsupp_single]
rw [C_mul_monomial, C_mul_monomial, mul_comm (v : ℤ) w, add_comm (n - m + k) n]
· exact fun h => h.2.ne rfl
· refine ⟨?_, add_lt_add_left key n⟩
rwa [add_comm, add_lt_add_iff_left, lt_add_iff_pos_left, tsub_pos_iff_lt]
· exact fun h => h.1.ne (add_comm k n)
· exact ⟨add_lt_add_right hkm n, add_lt_add_right hmn n⟩
· rw [← add_assoc, add_tsub_cancel_of_le hmn.le, add_comm]
exact fun h => h.1.ne rfl
· grind
· exact fun h => h.1.ne rfl
· exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) key
· exact fun h => asymm ((add_lt_add_iff_left k).mp h.1) (hkm.trans hmn)
