refactor: rename Algebra.Polynomial.Degree.Definitions → Algebra.Polynomial.Degree.Defs (leanprover-community#34449)

`Defs` is the standard name for files mainly containing definitions.

Author: vihdzp

Mathlib.lean

@@ -1064,7 +1064,7 @@ public import Mathlib.Algebra.Polynomial.Coeff
 public import Mathlib.Algebra.Polynomial.CoeffList
 public import Mathlib.Algebra.Polynomial.CoeffMem
 public import Mathlib.Algebra.Polynomial.Degree.CardPowDegree
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 public import Mathlib.Algebra.Polynomial.Degree.Domain
 public import Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
 public import Mathlib.Algebra.Polynomial.Degree.Lemmas

Mathlib/Algebra/Group/ForwardDiff.lean

@@ -12,7 +12,7 @@ public import Mathlib.Data.Nat.Choose.Sum
 public import Mathlib.Tactic.Abel
 public import Mathlib.Algebra.GroupWithZero.Action.Pi
 public import Mathlib.Algebra.Polynomial.Basic
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 public import Mathlib.Algebra.Polynomial.Eval.Degree
 
 /-!

Mathlib/Algebra/Polynomial/CoeffList.lean

@@ -5,7 +5,7 @@ Authors: Alex Meiburg
 -/
 module
 
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 public import Mathlib.Algebra.Polynomial.EraseLead
 public import Mathlib.Data.List.Range
 

…gebra/Polynomial/Degree/Definitions.lean …hlib/Algebra/Polynomial/Degree/Defs.leanMathlib/Algebra/Polynomial/Degree/Definitions.lean renamed to Mathlib/Algebra/Polynomial/Degree/Defs.lean Mathlib/Algebra/Polynomial/Degree/Definitions.lean renamed to Mathlib/Algebra/Polynomial/Degree/Defs.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
 module
 
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 public import Mathlib.Algebra.Polynomial.Monomial
 public import Mathlib.Data.Nat.SuccPred
 

Mathlib/Algebra/Polynomial/Degree/Monomial.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.GroupWithZero.Regular
 public import Mathlib.Algebra.Polynomial.Coeff
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 
 /-!
 # Lemmas for calculating the degree of univariate polynomials

Mathlib/Algebra/Polynomial/Degree/Operations.lean

@@ -6,7 +6,7 @@ Authors: Antoine Chambert-Loir
 module
 
 public import Mathlib.Algebra.MvPolynomial.Equiv
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 public import Mathlib.Data.Finsupp.MonomialOrder.DegLex
 public import Mathlib.RingTheory.Ideal.Maps
 public import Mathlib.RingTheory.MvPolynomial.Groebner

Mathlib/Combinatorics/Nullstellensatz.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau
 -/
 module
 
-public import Mathlib.Algebra.Polynomial.Degree.Definitions
+public import Mathlib.Algebra.Polynomial.Degree.Defs
 public import Mathlib.Algebra.Polynomial.Eval.Defs
 public import Mathlib.Tactic.Algebraize