Stream: general

Topic: constant polynomials

Jack J Garzella (Jun 17 2020 at 15:01):

I have the following example, which has a proof that seems quite long for the statement:

example {F : Type u} [field F] (a : F) : degree (X - C a) = 1 :=
begin
have deg_X_eq_one : degree (X : polynomial F) = 1,
{ have X_eq_one_mul_X_pow_one : (X : polynomial F) = C 1 * X ^ 1,
{ calc (X : polynomial F) = X ^ 1 : by ring_exp
...   = C 1 * X ^ 1 : by simp },
rw congr_arg degree X_eq_one_mul_X_pow_one,
apply @degree_monomial F 1 _ 1 (ne.symm field.zero_ne_one) },
have sub_eq_plus_minus : (X - C a) = (X + C (-a)),
{ simp [map_neg], ring },
rw congr_arg degree sub_eq_plus_minus,
have z_lt_o : (0 : with_bot ℕ) < (1 : with_bot ℕ),
{ have zero_eq_zero_coe : (0 : with_bot ℕ) = ↑(0 : ℕ),
{ by simp },
have one_eq_one_coe : (1 : with_bot ℕ) = ↑(1 : ℕ),
{ by simp },
simp [zero_eq_zero_coe, one_eq_one_coe, ←with_bot.some_eq_coe] },
(X : polynomial F)
(by {simp [deg_X_eq_one], exact z_lt_o})),
simp [deg_X_eq_one]
end


Particularly unruly is the part needed to prove that C 1 * X ^ 1 is the same as X, and the part where it takes a bunch of messing with coercions to prove that 0 < 1 remains true in the type with_bot ℕ, as my mathematical brain regards both of those statements as trivial. Any suggestions for shortening/simplifying the proof?

Chris Hughes (Jun 17 2020 at 15:07):

This is a lemma in the polynomial library degree_X_sub_C. I don't think there's a general nice method for proving these things, it would take me a while to prove this for more complicated polynomials, perhaps a tactic could be written to solve these.

Last updated: Dec 20 2023 at 11:08 UTC