## Stream: maths

### Topic: Definition of primitive

#### Thomas Browning (Apr 20 2021 at 06:27):

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?

@Aaron Anderson

#### Aaron Anderson (Apr 20 2021 at 06:34):

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

#### Aaron Anderson (Apr 20 2021 at 06:34):

It’s probably fine

Last updated: Jun 17 2021 at 18:14 UTC