Zulip Chat Archive

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?

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

@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: Dec 20 2023 at 11:08 UTC