[Merged by Bors] - feat: m/gcd m n and n coprime if m squarefree

[YaelDillies]

---

[alexjbest]

Looks like a good candidate for dot notation, also should be true if either m is Nonzero or n is Nonzero I think. So the hypothesis could be an or statement

[YaelDillies]

This can't reasonably be dot notation because the predicate is Squarefree, not Nat.Squarefree. The Squarefree m hypothesis already implies m ≠ 0 (and indeed the statement is false if we remove the n ≠ 0 assumption).

[alexjbest]

Ah right, this is Nat.gcd, we really should combine those at some point (I'd imagine this lemma would be true more generally then).

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported