English
If k is an integral domain and a1_0 ≠ 0, a2_0 ≠ 0, then the degree of succNthDefiningPoly(p,n,a1,a2,bs) equals p.
Русский
Если k — интегральная область, а a1_0 ≠ 0 и a2_0 ≠ 0, то deg succNthDefiningPoly(p,n,a1,a2,bs) = p.
LaTeX
$$\deg(\operatorname{succNthDefiningPoly}(p,n,a_1,a_2,bs)) = p$$
Lean4
theorem succNthDefiningPoly_degree [IsDomain k] (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0)
(ha₂ : a₂.coeff 0 ≠ 0) : (succNthDefiningPoly p n a₁ a₂ bs).degree = p :=
by
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = (p : WithBot ℕ) :=
by
rw [degree_mul, degree_C]
· simp only [Nat.cast_withBot, add_zero, degree_X, degree_pow, Nat.smul_one_eq_cast]
· exact pow_ne_zero _ ha₁
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = (p : WithBot ℕ) :=
by
rw [degree_sub_eq_left_of_degree_lt, this]
rw [this, degree_mul, degree_C, degree_X, add_zero]
· exact mod_cast hp.out.one_lt
· exact pow_ne_zero _ ha₂
rw [succNthDefiningPoly, degree_add_eq_left_of_degree_lt, this]
apply lt_of_le_of_lt degree_C_le
rw [this]
exact mod_cast hp.out.pos
