mathlib3
e483298a - feat(ring_theory/unique_factorization_domain): API for coprime, coprime factor of a power is a power (#4049)

Commit

5 years ago

feat(ring_theory/unique_factorization_domain): API for coprime, coprime factor of a power is a power (#4049) Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>

References

#4925 - Make prime-avoidance branch build

Author

paulvanwamelen

Parents

40f582b9

mathlib3 e483298a - feat(ring_theory/unique_factorization_domain): API for coprime, coprime factor of a power is a power (#4049)

mathlib3
e483298a - feat(ring_theory/unique_factorization_domain): API for coprime, coprime factor of a power is a power (#4049)