chore: rename IsRoot.definition back to IsRoot.def (#11999)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Archive/Imo/Imo2006Q5.lean

@@ -150,8 +150,8 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
   -- Otherwise, take a, b with P(a) = b, P(b) = a, a ≠ b.
   · rcases Finset.not_subset.1 H with ⟨a, ha, hab⟩
     replace ha := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ha)
-    rw [IsRoot.definition, eval_sub, eval_comp, eval_X, sub_eq_zero] at ha
-    rw [Multiset.mem_toFinset, mem_roots hPX', IsRoot.definition, eval_sub, eval_X, sub_eq_zero]
+    rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ha
+    rw [Multiset.mem_toFinset, mem_roots hPX', IsRoot.def, eval_sub, eval_X, sub_eq_zero]
       at hab
     set b := P.eval a
     -- More auxiliary lemmas on degrees.
@@ -176,8 +176,8 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
     · -- Let t be a root of P(P(t)) - t, define u = P(t).
       intro t ht
       replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
-      rw [IsRoot.definition, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
-      simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.definition,
+      rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
+      simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
         eval_sub, eval_add, eval_X, eval_C, eval_int_cast, Int.cast_id, zero_add]
       -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
       -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
@@ -201,8 +201,8 @@ theorem imo2006_q5 {P : Polynomial ℤ} (hP : 1 < P.natDegree) {k : ℕ} (hk : 0
   have hP' : P.comp P - X ≠ 0 := by
     simpa [Nat.iterate] using Polynomial.iterate_comp_sub_X_ne hP zero_lt_two
   replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
-  rw [IsRoot.definition, eval_sub, iterate_comp_eval, eval_X, sub_eq_zero] at ht
-  rw [Multiset.mem_toFinset, mem_roots hP', IsRoot.definition, eval_sub, eval_comp, eval_X,
+  rw [IsRoot.def, eval_sub, iterate_comp_eval, eval_X, sub_eq_zero] at ht
+  rw [Multiset.mem_toFinset, mem_roots hP', IsRoot.def, eval_sub, eval_comp, eval_X,
     sub_eq_zero]
   exact Polynomial.isPeriodicPt_eval_two ⟨k, hk, ht⟩
 #align imo2006_q5 imo2006_q5

Mathlib/Algebra/LinearRecurrence.lean

@@ -216,7 +216,7 @@ def charPoly : α[X] :=
   `q` is a root of `E`'s characteristic polynomial. -/
 theorem geom_sol_iff_root_charPoly (q : α) :
     (E.IsSolution fun n ↦ q ^ n) ↔ E.charPoly.IsRoot q := by
-  rw [charPoly, Polynomial.IsRoot.definition, Polynomial.eval]
+  rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]
   simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial,
     Polynomial.eval₂_sub]
   constructor

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

@@ -85,11 +85,9 @@ theorem monic_of_subsingleton [Subsingleton R] (p : R[X]) : Monic p :=
   Subsingleton.elim _ _
 #align polynomial.monic_of_subsingleton Polynomial.monic_of_subsingleton
 
--- Adaptation note: 2024-03-15
--- Renamed to avoid the reserved name `Monic.def`.
-theorem Monic.def' : Monic p ↔ leadingCoeff p = 1 :=
+theorem Monic.def : Monic p ↔ leadingCoeff p = 1 :=
   Iff.rfl
-#align polynomial.monic.def Polynomial.Monic.def'
+#align polynomial.monic.def Polynomial.Monic.def
 
 instance Monic.decidable [DecidableEq R] : Decidable (Monic p) := by unfold Monic; infer_instance
 #align polynomial.monic.decidable Polynomial.Monic.decidable
@@ -1204,7 +1202,7 @@ theorem eq_C_coeff_zero_iff_natDegree_eq_zero : p = C (p.coeff 0) ↔ p.natDegre
   ⟨fun h ↦ by rw [h, natDegree_C], eq_C_of_natDegree_eq_zero⟩
 
 theorem eq_one_of_monic_natDegree_zero (hf : p.Monic) (hfd : p.natDegree = 0) : p = 1 := by
-  rw [Monic.def', leadingCoeff, hfd] at hf
+  rw [Monic.def, leadingCoeff, hfd] at hf
   rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]
 
 theorem ne_zero_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : p ≠ 0 :=

Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

@@ -67,11 +67,9 @@ def TrailingMonic (p : R[X]) :=
   trailingCoeff p = (1 : R)
 #align polynomial.trailing_monic Polynomial.TrailingMonic
 
--- Adaptation note: 2024-03-15: this was called `def`.
--- Should lean be changed to allow that as a name again?
-theorem TrailingMonic.definition : TrailingMonic p ↔ trailingCoeff p = 1 :=
+theorem TrailingMonic.def : TrailingMonic p ↔ trailingCoeff p = 1 :=
   Iff.rfl
-#align polynomial.trailing_monic.def Polynomial.TrailingMonic.definition
+#align polynomial.trailing_monic.def Polynomial.TrailingMonic.def
 
 instance TrailingMonic.decidable [DecidableEq R] : Decidable (TrailingMonic p) :=
   inferInstanceAs <| Decidable (trailingCoeff p = (1 : R))

Mathlib/Algebra/Polynomial/Div.lean

@@ -278,7 +278,7 @@ theorem degree_add_divByMonic (hq : Monic q) (h : degree q ≤ degree p) :
   nontriviality R
   have hdiv0 : p /ₘ q ≠ 0 := by rwa [Ne.def, divByMonic_eq_zero_iff hq, not_lt]
   have hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by
-    rwa [Monic.def'.1 hq, one_mul, Ne.def, leadingCoeff_eq_zero]
+    rwa [Monic.def.1 hq, one_mul, Ne.def, leadingCoeff_eq_zero]
   have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
     calc
       degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
@@ -364,7 +364,7 @@ theorem div_modByMonic_unique {f g} (q r : R[X]) (hg : Monic g)
           degree g ≤ degree g + degree (q - f /ₘ g) := by
             erw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf, WithBot.coe_le_coe]
             exact Nat.le_add_right _ _
-          _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def'.1 hg]
+          _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
   exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩
 #align polynomial.div_mod_by_monic_unique Polynomial.div_modByMonic_unique
 
@@ -381,7 +381,7 @@ theorem map_mod_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) :
           _ = _ :=
             Eq.symm <|
               degree_map_eq_of_leadingCoeff_ne_zero _
-                (by rw [Monic.def'.1 hq, f.map_one]; exact one_ne_zero)⟩
+                (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
   exact ⟨this.1.symm, this.2.symm⟩
 #align polynomial.map_mod_div_by_monic Polynomial.map_mod_divByMonic
 
@@ -406,7 +406,7 @@ theorem modByMonic_eq_zero_iff_dvd (hq : Monic q) : p %ₘ q = 0 ↔ q ∣ p :=
       hpq0 <|
         leadingCoeff_eq_zero.1
           (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
-    have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def'.1 hq, one_mul]
+    have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
     rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
       degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this
     exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.some_lt_some.1 this)⟩
@@ -615,7 +615,7 @@ set_option linter.uppercaseLean3 false in
 
 theorem mul_divByMonic_eq_iff_isRoot : (X - C a) * (p /ₘ (X - C a)) = p ↔ IsRoot p a :=
   ⟨fun h => by
-    rw [← h, IsRoot.definition, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
+    rw [← h, IsRoot.def, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
     fun h : p.eval a = 0 => by
     conv_rhs =>
         rw [← modByMonic_add_div p (monic_X_sub_C a)]
@@ -694,7 +694,7 @@ theorem eval_divByMonic_pow_rootMultiplicity_ne_zero {p : R[X]} (a : R) (hp : p
     eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0 := by
   classical
   haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
-  rw [Ne.def, ← IsRoot.definition, ← dvd_iff_isRoot]
+  rw [Ne.def, ← IsRoot.def, ← dvd_iff_isRoot]
   rintro ⟨q, hq⟩
   have := pow_mul_divByMonic_rootMultiplicity_eq p a
   rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, dif_neg hp] at this

Mathlib/Algebra/Polynomial/Eval.lean

@@ -498,12 +498,10 @@ instance IsRoot.decidable [DecidableEq R] : Decidable (IsRoot p a) := by
   unfold IsRoot; infer_instance
 #align polynomial.is_root.decidable Polynomial.IsRoot.decidable
 
--- Adaptation note: 2024-03-15: this was called `def`.
--- Should lean be changed to allow that as a name again?
 @[simp]
-theorem IsRoot.definition : IsRoot p a ↔ p.eval a = 0 :=
+theorem IsRoot.def : IsRoot p a ↔ p.eval a = 0 :=
   Iff.rfl
-#align polynomial.is_root.def Polynomial.IsRoot.definition
+#align polynomial.is_root.def Polynomial.IsRoot.def
 
 theorem IsRoot.eq_zero (h : IsRoot p x) : eval x p = 0 :=
   h
@@ -1160,11 +1158,11 @@ theorem coe_compRingHom_apply (p q : R[X]) : (compRingHom q : R[X] → R[X]) p =
 #align polynomial.coe_comp_ring_hom_apply Polynomial.coe_compRingHom_apply
 
 theorem root_mul_left_of_isRoot (p : R[X]) {q : R[X]} : IsRoot q a → IsRoot (p * q) a := fun H => by
-  rw [IsRoot, eval_mul, IsRoot.definition.1 H, mul_zero]
+  rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
 #align polynomial.root_mul_left_of_is_root Polynomial.root_mul_left_of_isRoot
 
 theorem root_mul_right_of_isRoot {p : R[X]} (q : R[X]) : IsRoot p a → IsRoot (p * q) a := fun H =>
-  by rw [IsRoot, eval_mul, IsRoot.definition.1 H, zero_mul]
+  by rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
 #align polynomial.root_mul_right_of_is_root Polynomial.root_mul_right_of_isRoot
 
 theorem eval₂_multiset_prod (s : Multiset R[X]) (x : S) :
@@ -1323,7 +1321,7 @@ theorem eval_sub (p q : R[X]) (x : R) : (p - q).eval x = p.eval x - q.eval x :=
 #align polynomial.eval_sub Polynomial.eval_sub
 
 theorem root_X_sub_C : IsRoot (X - C a) b ↔ a = b := by
-  rw [IsRoot.definition, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
+  rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
 #align polynomial.root_X_sub_C Polynomial.root_X_sub_C
 
 @[simp]

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -320,12 +320,12 @@ theorem mod_def : p % q = p %ₘ (q * C (leadingCoeff q)⁻¹) := rfl
 
 theorem modByMonic_eq_mod (p : R[X]) (hq : Monic q) : p %ₘ q = p % q :=
   show p %ₘ q = p %ₘ (q * C (leadingCoeff q)⁻¹) by
-    simp only [Monic.def'.1 hq, inv_one, mul_one, C_1]
+    simp only [Monic.def.1 hq, inv_one, mul_one, C_1]
 #align polynomial.mod_by_monic_eq_mod Polynomial.modByMonic_eq_mod
 
 theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
   show p /ₘ q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹)) by
-    simp only [Monic.def'.1 hq, inv_one, C_1, one_mul, mul_one]
+    simp only [Monic.def.1 hq, inv_one, C_1, one_mul, mul_one]
 #align polynomial.div_by_monic_eq_div Polynomial.divByMonic_eq_div
 
 theorem mod_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a) :=

Mathlib/Algebra/Polynomial/Monic.lean

@@ -57,7 +57,7 @@ theorem Monic.as_sum (hp : p.Monic) :
 
 theorem ne_zero_of_ne_zero_of_monic (hp : p ≠ 0) (hq : Monic q) : q ≠ 0 := by
   rintro rfl
-  rw [Monic.def', leadingCoeff_zero] at hq
+  rw [Monic.def, leadingCoeff_zero] at hq
   rw [← mul_one p, ← C_1, ← hq, C_0, mul_zero] at hp
   exact hp rfl
 #align polynomial.ne_zero_of_ne_zero_of_monic Polynomial.ne_zero_of_ne_zero_of_monic
@@ -121,8 +121,8 @@ theorem Monic.mul (hp : Monic p) (hq : Monic q) : Monic (p * q) :=
     Subsingleton.elim _ _
   else by
     have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
-      simp [Monic.def'.1 hp, Monic.def'.1 hq, Ne.symm h0]
-    rw [Monic.def', leadingCoeff_mul' this, Monic.def'.1 hp, Monic.def'.1 hq, one_mul]
+      simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
+    rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
 #align polynomial.monic.mul Polynomial.Monic.mul
 
 theorem Monic.pow (hp : Monic p) : ∀ n : ℕ, Monic (p ^ n)
@@ -142,13 +142,13 @@ theorem Monic.add_of_right (hq : Monic q) (hpq : degree p < degree q) : Monic (p
 
 theorem Monic.of_mul_monic_left (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic := by
   contrapose! hpq
-  rw [Monic.def'] at hpq ⊢
+  rw [Monic.def] at hpq ⊢
   rwa [leadingCoeff_monic_mul hp]
 #align polynomial.monic.of_mul_monic_left Polynomial.Monic.of_mul_monic_left
 
 theorem Monic.of_mul_monic_right (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic := by
   contrapose! hpq
-  rw [Monic.def'] at hpq ⊢
+  rw [Monic.def] at hpq ⊢
   rwa [leadingCoeff_mul_monic hq]
 #align polynomial.monic.of_mul_monic_right Polynomial.Monic.of_mul_monic_right
 
@@ -164,7 +164,7 @@ theorem natDegree_eq_zero_iff_eq_one (hp : p.Monic) : p.natDegree = 0 ↔ p = 1
     rw [← Polynomial.degree_le_zero_iff]
     rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h
   rw [this]
-  rw [← h, ← Polynomial.leadingCoeff, Monic.def'.1 hp, C_1]
+  rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]
 #align polynomial.monic.nat_degree_eq_zero_iff_eq_one Polynomial.Monic.natDegree_eq_zero_iff_eq_one
 
 @[simp]
@@ -526,7 +526,7 @@ theorem leadingCoeff_smul_of_smul_regular {S : Type*} [Monoid S] [DistribMulActi
 
 theorem monic_of_isUnit_leadingCoeff_inv_smul (h : IsUnit p.leadingCoeff) :
     Monic (h.unit⁻¹ • p) := by
-  rw [Monic.def', leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
+  rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
   obtain ⟨k, hk⟩ := h
   simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]
   simp [Units.ext_iff, IsUnit.unit_spec]

Mathlib/Algebra/Polynomial/RingDivision.lean

@@ -570,7 +570,7 @@ open Multiset
 
 theorem prime_X_sub_C (r : R) : Prime (X - C r) :=
   ⟨X_sub_C_ne_zero r, not_isUnit_X_sub_C r, fun _ _ => by
-    simp_rw [dvd_iff_isRoot, IsRoot.definition, eval_mul, mul_eq_zero]
+    simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]
     exact id⟩
 set_option linter.uppercaseLean3 false in
 #align polynomial.prime_X_sub_C Polynomial.prime_X_sub_C
@@ -739,7 +739,7 @@ theorem isRoot_of_mem_roots (h : a ∈ p.roots) : IsRoot p a :=
 
 -- Porting note: added during port.
 lemma mem_roots_iff_aeval_eq_zero (w : p ≠ 0) : x ∈ roots p ↔ aeval x p = 0 := by
-  rw [mem_roots w, IsRoot.definition, aeval_def, eval₂_eq_eval_map]
+  rw [mem_roots w, IsRoot.def, aeval_def, eval₂_eq_eval_map]
   simp
 
 theorem card_le_degree_of_subset_roots {p : R[X]} {Z : Finset R} (h : Z.val ⊆ p.roots) :
@@ -784,7 +784,7 @@ theorem roots.le_of_dvd (h : q ≠ 0) : p ∣ q → roots p ≤ roots q := by
 #align polynomial.roots.le_of_dvd Polynomial.roots.le_of_dvd
 
 theorem mem_roots_sub_C' {p : R[X]} {a x : R} : x ∈ (p - C a).roots ↔ p ≠ C a ∧ p.eval x = a := by
-  rw [mem_roots', IsRoot.definition, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]
+  rw [mem_roots', IsRoot.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C]
 set_option linter.uppercaseLean3 false in
 #align polynomial.mem_roots_sub_C' Polynomial.mem_roots_sub_C'
 
@@ -932,7 +932,7 @@ def nthRoots (n : ℕ) (a : R) : Multiset R :=
 
 @[simp]
 theorem mem_nthRoots {n : ℕ} (hn : 0 < n) {a x : R} : x ∈ nthRoots n a ↔ x ^ n = a := by
-  rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.definition, eval_sub, eval_C, eval_pow,
+  rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
     eval_X, sub_eq_zero]
 #align polynomial.mem_nth_roots Polynomial.mem_nthRoots
 
@@ -1018,7 +1018,7 @@ theorem one_mem_nthRootsFinset (hn : 0 < n) : 1 ∈ nthRootsFinset n R := by
 end NthRoots
 
 theorem Monic.comp (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic := by
-  rw [Monic.def', leadingCoeff_comp h, Monic.def'.1 hp, Monic.def'.1 hq, one_pow, one_mul]
+  rw [Monic.def, leadingCoeff_comp h, Monic.def.1 hp, Monic.def.1 hq, one_pow, one_mul]
 #align polynomial.monic.comp Polynomial.Monic.comp
 
 theorem Monic.comp_X_add_C (hp : p.Monic) (r : R) : (p.comp (X + C r)).Monic := by
@@ -1084,7 +1084,7 @@ theorem aroots_def (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] :
 
 theorem mem_aroots' [CommRing S] [IsDomain S] [Algebra T S] {p : T[X]} {a : S} :
     a ∈ p.aroots S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0 := by
-  rw [mem_roots', IsRoot.definition, ← eval₂_eq_eval_map, aeval_def]
+  rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]
 
 theorem mem_aroots [CommRing S] [IsDomain S] [Algebra T S]
     [NoZeroSMulDivisors T S] {p : T[X]} {a : S} : a ∈ p.aroots S ↔ p ≠ 0 ∧ aeval a p = 0 := by
@@ -1383,7 +1383,7 @@ lemma eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R]
     _ ≤ Finset.card p.roots.toFinset := Finset.card_mono ?_
   intro _
   simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
-    IsRoot.definition, forall_exists_index, hp, not_false_eq_true]
+    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
   rintro x rfl
   exact heval _
 

Mathlib/Algebra/Polynomial/Splits.lean

@@ -233,12 +233,10 @@ theorem splits_iff (f : K[X]) :
 #align polynomial.splits_iff Polynomial.splits_iff
 
 /-- This lemma is for polynomials over a field. -/
--- Adaptation note: 2024-03-15
--- Renamed to avoid the reserved name `Splits.def`.
-theorem Splits.def' {i : K →+* L} {f : K[X]} (h : Splits i f) :
+theorem Splits.def {i : K →+* L} {f : K[X]} (h : Splits i f) :
     f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1 :=
   (splits_iff i f).mp h
-#align polynomial.splits.def Polynomial.Splits.def'
+#align polynomial.splits.def Polynomial.Splits.def
 
 theorem splits_of_splits_mul {f g : K[X]} (hfg : f * g ≠ 0) (h : Splits i (f * g)) :
     Splits i f ∧ Splits i g :=
@@ -411,7 +409,7 @@ theorem splits_of_splits_id {f : K[X]} : Splits (RingHom.id K) f → Splits i f
     fun a p ha0 hp ih hfi =>
     splits_mul _
       (splits_of_degree_eq_one _
-        ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.def'.resolve_left hp.1 hp.irreducible
+        ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.def.resolve_left hp.1 hp.irreducible
           (by rw [map_id])))
       (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2)
 #align polynomial.splits_of_splits_id Polynomial.splits_of_splits_id

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -191,18 +191,16 @@ alias ⟨IsLittleO.bound, IsLittleO.of_bound⟩ := isLittleO_iff
 #align asymptotics.is_o.bound Asymptotics.IsLittleO.bound
 #align asymptotics.is_o.of_bound Asymptotics.IsLittleO.of_bound
 
--- Adaptation note: 2024-03-15: this was called `def`.
--- Should lean be changed to allow that as a name again?
-theorem IsLittleO.definition (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
+theorem IsLittleO.def (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
   isLittleO_iff.1 h hc
-#align asymptotics.is_o.def Asymptotics.IsLittleO.definition
+#align asymptotics.is_o.def Asymptotics.IsLittleO.def
 
 theorem IsLittleO.def' (h : f =o[l] g) (hc : 0 < c) : IsBigOWith c l f g :=
   isBigOWith_iff.2 <| isLittleO_iff.1 h hc
 #align asymptotics.is_o.def' Asymptotics.IsLittleO.def'
 
 theorem IsLittleO.eventuallyLE (h : f =o[l] g) : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖ := by
-  simpa using h.definition zero_lt_one
+  simpa using h.def zero_lt_one
 
 end Defs
 
@@ -280,7 +278,7 @@ theorem isLittleO_iff_nat_mul_le_aux (h₀ : (∀ x, 0 ≤ ‖f x‖) ∨ ∀ x,
     f =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g x‖ := by
   constructor
   · rintro H (_ | n)
-    · refine' (H.definition one_pos).mono fun x h₀' => _
+    · refine' (H.def one_pos).mono fun x h₀' => _
       rw [Nat.cast_zero, zero_mul]
       refine' h₀.elim (fun hf => (hf x).trans _) fun hg => hg x
       rwa [one_mul] at h₀'

Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

@@ -243,7 +243,7 @@ theorem hasIntegral_GP_pderiv (f : (Fin (n + 1) → ℝ) → E)
         an estimate we proved earlier in this file. -/
     rcases exists_pos_mul_lt ε0 (2 * c) with ⟨ε', ε'0, hlt⟩
     rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1
-      ((Hd x hx).isLittleO.definition ε'0) with ⟨δ, δ0, Hδ⟩
+      ((Hd x hx).isLittleO.def ε'0) with ⟨δ, δ0, Hδ⟩
     refine' ⟨δ, δ0, fun J hle hJδ hxJ hJc => _⟩
     simp only [BoxAdditiveMap.volume_apply, Box.volume_apply, dist_eq_norm]
     refine' (norm_volume_sub_integral_face_upper_sub_lower_smul_le _