English
Under the hypotheses, applying reduction to f yields m.degree(m.reduce hb f) < m.degree f, provided m.degree f ≠ 0 and hb expresses a unit leading coefficient.
Русский
При условии редукции f полиномом b с единичным ведущим коэффициентом даёт deg_m( reduce f ) < deg_m f при deg_m f ≠ 0.
LaTeX
$$$\\deg_m(m.\\mathrm{reduce} \\; hb\\; f) \\; <_m \\; \\deg_m f$$$
Lean4
theorem degree_reduce_lt {f b : MvPolynomial σ R} (hb : IsUnit (m.leadingCoeff b)) (hbf : m.degree b ≤ m.degree f)
(hf : m.degree f ≠ 0) : m.degree (m.reduce hb f) ≺[m] m.degree f :=
by
have H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b :=
by
classical
rw [degree_monomial, if_neg]
· ext d
rw [tsub_add_cancel_of_le hbf]
· simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
intro hf0
apply hf
simp [hf0]
have H' : coeff (m.degree f) (m.reduce hb f) = 0 :=
by
simp only [reduce, coeff_sub, sub_eq_zero]
nth_rewrite 2 [H]
rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc, IsUnit.mul_val_inv, one_mul, ←
leadingCoeff]
rw [lt_iff_le_and_ne]
constructor
·
classical
apply le_trans degree_sub_le
simp only [sup_le_iff, le_refl, true_and]
apply le_of_le_of_eq degree_mul_le
rw [m.toSyn.injective.eq_iff]
exact H.symm
· intro K
simp only [EmbeddingLike.apply_eq_iff_eq] at K
nth_rewrite 1 [← K] at H'
rw [← leadingCoeff, leadingCoeff_eq_zero_iff] at H'
rw [H', degree_zero] at K
exact hf K.symm
