chore(*): rename is_unit_pow to is_unit.pow (#4329)

enable dot notation by renaming
is_unit_pow to is_unit.pow

src/algebra/associated.lean

@@ -12,7 +12,7 @@ import algebra.divisibility
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 
-lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
+lemma is_unit.pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
 
 theorem is_unit_iff_dvd_one [comm_monoid α] {x : α} : is_unit x ↔ x ∣ 1 :=

src/ring_theory/multiplicity.lean

@@ -52,7 +52,7 @@ lemma not_finite_iff_forall {a b : α} : (¬ finite a b) ↔ ∀ n : ℕ, a ^ n
   by simp [finite, multiplicity, not_not]; tauto⟩
 
 lemma not_unit_of_finite {a b : α} (h : finite a b) : ¬is_unit a :=
-let ⟨n, hn⟩ := h in mt (is_unit_iff_forall_dvd.1 ∘ is_unit_pow (n + 1)) $
+let ⟨n, hn⟩ := h in mt (is_unit_iff_forall_dvd.1 ∘ is_unit.pow (n + 1)) $
 λ h, hn (h b)
 
 lemma finite_of_finite_mul_left {a b c : α} : finite a (b * c) → finite a c :=
@@ -123,7 +123,7 @@ get_eq_iff_eq_some.2 (eq_some_iff.2 ⟨dvd_refl _,
   by simpa [is_unit_iff_dvd_one.symm] using not_unit_of_finite ha⟩)
 
 @[simp] lemma multiplicity_unit {a : α} (b : α) (ha : is_unit a) : multiplicity a b = ⊤ :=
-eq_top_iff.2 (λ _, is_unit_iff_forall_dvd.1 (is_unit_pow _ ha) _)
+eq_top_iff.2 (λ _, is_unit_iff_forall_dvd.1 (ha.pow _) _)
 
 @[simp] lemma one_left (b : α) : multiplicity 1 b = ⊤ := by simp [eq_top_iff]
 

src/ring_theory/polynomial/rational_root.lean

@@ -71,7 +71,7 @@ begin
   { simp only [coeff_scale_roots, nat.sub_zero] at this,
     haveI := classical.prop_decidable,
     by_cases hr : f.num r = 0,
-    { obtain ⟨u, hu⟩ := is_unit_pow p.nat_degree (f.is_unit_denom_of_num_eq_zero hr),
+    { obtain ⟨u, hu⟩ := (f.is_unit_denom_of_num_eq_zero hr).pow p.nat_degree,
       rw ←hu at this,
       exact units.dvd_mul_right.mp this },
     { refine dvd_of_dvd_mul_left_of_no_prime_of_factor hr _ this,