Zulip Chat Archive

Stream: maths

Topic: Definition of primitive


view this post on Zulip 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?

view this post on Zulip Thomas Browning (Apr 20 2021 at 06:27):

@Aaron Anderson

view this post on Zulip Aaron Anderson (Apr 20 2021 at 06:34):

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

view this post on Zulip Aaron Anderson (Apr 20 2021 at 06:34):

It’s probably fine


Last updated: Jun 17 2021 at 18:14 UTC