chore(data/polynomial): use dot notation for sub lemmas (#13799)

To match the additive versions

Author: alexjbest

src/data/polynomial/monic.lean

@@ -376,11 +376,11 @@ begin
       nat_degree_one]
 end
 
-lemma monic_sub_of_left {p q : R[X]} (hp : monic p) (hpq : degree q < degree p) :
+lemma monic.sub_of_left {p q : R[X]} (hp : monic p) (hpq : degree q < degree p) :
   monic (p - q) :=
 by { rw sub_eq_add_neg, apply hp.add_of_left, rwa degree_neg }
 
-lemma monic_sub_of_right {p q : R[X]}
+lemma monic.sub_of_right {p q : R[X]}
   (hq : q.leading_coeff = -1) (hpq : degree p < degree q) : monic (p - q) :=
 have (-q).coeff (-q).nat_degree = 1 :=
 by rw [nat_degree_neg, coeff_neg, show q.coeff q.nat_degree = -1, from hq, neg_neg],

src/ring_theory/power_basis.lean

@@ -209,7 +209,7 @@ nat_degree_eq_of_degree_eq_some pb.degree_minpoly_gen
 
 lemma minpoly_gen_monic (pb : power_basis A S) : monic (minpoly_gen pb) :=
 begin
-  apply monic_sub_of_left (monic_X_pow _) _,
+  apply (monic_X_pow _).sub_of_left _,
   rw degree_X_pow,
   exact degree_sum_fin_lt _
 end