feat(ring_theory/unique_factorization_domain): API for coprime, coprime factor of a power is a power

[paulvanwamelen]

---

Main result is is_pow_of_coprime. I want this for a proof of the n=4 case of fermat.

[awainverse]

I've been working on some related stuff at the branch mathlib:ufm. I was thinking that we would take gcd a b = 1 as the definition of coprime a b, but I'm not sure which is better. Yours is more general, but mine has nice properties in a general gcd_monoid, and they only coincide in a ufm.

[kckennylau]

Suggested change

	def associates_coprime (a b : associates α) : Prop :=
	∀ (p : associates α), prime p → p ∣ a → ¬ p ∣ b
	def associates_coprime (a b : associates α) : Prop :=
	∀ (p : associates α), prime p → p ≤ a → ¬ p ≤ b

When in Rome, do as the Romans do: you'll see that the lemmas around this all use ≤ instead of ∣, and there is even an explicit theorem dvd_eq_le saying that ∣ = ≤ (not the other way round!)

[paulvanwamelen]

This definition has to move, but when I do I'll keep this change in mind.

[kckennylau]

Suggested change

	begin
	intros p h₁ hb ha,
	exact h _ h₁ ha hb
	end
	λ p h₁ hb ha, h p h₁ ha hb

[kckennylau]

If you use the "Files changed" tab, you can apply the changes in one commit instead of five.

[paulvanwamelen]

I'll open a new one with a clean commit that should be easier to review.