Definition of primitive

Stream: maths

[Thomas Browning]

Currently polynomial.is_primitive is defined as p.content = 1, which requires a gcd_monoid assumption. However, the lemma is_primitive_iff_is_unit_of_C_dvd states that p.is_primitive ↔ ∀ (r : R), C r ∣ p → is_unit r. In light of this, would it make sense to define polynomial.is_primitive as ∀ (r : R), C r ∣ p → is_unit r?

[Thomas Browning]

@Aaron Anderson

[Aaron Anderson]

That sounds like a better definition unless refactoring the current API is a pain

[Aaron Anderson]

It’s probably fine