content

Stream: new members

[vxctyxeha]

is there simpler way to solve this

import Mathlib

open Polynomial
lemma p_content : ( X^3 +  3 * X^2 - 3 : Polynomial ℤ).content = 1 := by sorry

[vxctyxeha]

sometimes a good tactic is worthy 100 lines

[Riccardo Brasca]

We know that primitive polynomials have content equal to 1, and that monic polynomials are primitive. Using monicity! to prove that the polynomial is monic this is probably a one-liner.