chore(algebra/squarefree): rename squarefree_of_dvd_of_squarefree f…

…or dot notation (#17071)

As suggested in #16999, this name is quite long and should get dot notation. I'm not totally convinced by the name but can't come up with a better one myself at the moment.



Co-authored-by: Anne Baanen <t.baanen@vu.nl>
Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

src/algebra/squarefree.lean

@@ -77,7 +77,7 @@ lemma squarefree.of_mul_left [comm_monoid R] {m n : R} (hmn : squarefree (m * n)
 lemma squarefree.of_mul_right [comm_monoid R] {m n : R} (hmn : squarefree (m * n)) : squarefree n :=
 (λ p hp, hmn p (dvd_mul_of_dvd_right hp m))
 
-lemma squarefree_of_dvd_of_squarefree [comm_monoid R]
+lemma squarefree.squarefree_of_dvd [comm_monoid R]
   {x y : R} (hdvd : x ∣ y) (hsq : squarefree y) :
   squarefree x :=
 λ a h, hsq _ (h.trans hdvd)
@@ -88,11 +88,11 @@ variables {α : Type*} [cancel_comm_monoid_with_zero α] [gcd_monoid α]
 
 lemma squarefree.gcd_right (a : α) {b : α} (hb : squarefree b) :
   squarefree (gcd a b) :=
-squarefree_of_dvd_of_squarefree (gcd_dvd_right _ _) hb
+hb.squarefree_of_dvd (gcd_dvd_right _ _)
 
 lemma squarefree.gcd_left {a : α} (b : α) (ha : squarefree a) :
   squarefree (gcd a b) :=
-squarefree_of_dvd_of_squarefree (gcd_dvd_left _ _) ha
+ha.squarefree_of_dvd (gcd_dvd_left _ _)
 
 end squarefree_gcd_of_squarefree
 

src/data/nat/squarefree.lean

@@ -84,7 +84,7 @@ begin
   refine ⟨λ h, _, by { rintro ⟨hn, rfl⟩, simpa }⟩,
   rcases eq_or_ne n 0 with rfl | hn₀,
   { simpa [zero_pow hk.bot_lt] using h },
-  refine ⟨squarefree_of_dvd_of_squarefree (dvd_pow_self _ hk) h, by_contradiction $ λ h₁, _⟩,
+  refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction $ λ h₁, _⟩,
   have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩,
   apply hn (nat.is_unit_iff.1 (h _ _)),
   rw ←sq,