degree of a polynomial

Stream: Is there code for X?

[Michael Stoll]

@Damiano Testa What is the best proof of

example {F} [field F] : degree (polynomial.X ^ 4 + polynomial.C 1 : polynomial F) ≠ 0 := sorry

?
I think you were implementing a tactic for stuff like this, but I can't find the topic right now...

[Damiano Testa]

The tactic is very simple at the moment and is here.

[Damiano Testa]

For the moment, it works with nat_degree and equalities. So, it might prove

example {F} [field F] : degree (polynomial.X ^ 4 + polynomial.C 1 : polynomial F) = 4

[Damiano Testa]

The tactic linked above does not yet "work out of the box". Let me see if I can get the statement that I wrote to work.

[Damiano Testa]

If you want to prove your statement, I still think that you might find it easier to prove the stronger

example {F} [field F] : degree (polynomial.X ^ 4 + polynomial.C 1 : polynomial F) = 4 :=

[Damiano Testa]

(I know my way around nat_degree better than degree and would use docs#polynomial.nat_degree_add_eq_left_of_nat_degree_lt.)

[Damiano Testa]

Ah, docs#polynomial.degree_add_eq_left_of_degree_lt seems to exist.

[Damiano Testa]

After that, you are left with docs#polynomial.degree_X_pow (?) and docs#polynomial.degree_C (?). Edit: the links should work.