From 73e85f2c867e3611249671978ecc4085c61d9eeb Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 21 Mar 2024 08:50:28 +0000 Subject: [PATCH] chore: rename away from 'def' (#11548) This will become an error in 2024-03-16 nightly, possibly not permanently. Co-authored-by: Scott Morrison --- Archive/Imo/Imo2006Q5.lean | 16 ++++---- Mathlib/Algebra/LinearRecurrence.lean | 2 +- Mathlib/Analysis/Asymptotics/Asymptotics.lean | 10 +++-- .../BoxIntegral/DivergenceTheorem.lean | 4 +- .../InverseFunctionTheorem/FDeriv.lean | 2 +- Mathlib/Analysis/Calculus/Rademacher.lean | 2 +- .../SpecialFunctions/NonIntegrable.lean | 2 +- Mathlib/Analysis/SpecificLimits/Normed.lean | 2 +- Mathlib/CategoryTheory/Generator.lean | 40 +++++++++++-------- .../CategoryTheory/Preadditive/Generator.lean | 4 +- Mathlib/CategoryTheory/Subterminal.lean | 8 ++-- .../Data/Polynomial/Degree/Definitions.lean | 8 ++-- .../Polynomial/Degree/TrailingDegree.lean | 6 ++- Mathlib/Data/Polynomial/Div.lean | 12 +++--- Mathlib/Data/Polynomial/Eval.lean | 12 +++--- Mathlib/Data/Polynomial/FieldDivision.lean | 5 ++- Mathlib/Data/Polynomial/Monic.lean | 14 +++---- Mathlib/Data/Polynomial/RingDivision.lean | 14 +++---- Mathlib/Data/Polynomial/Splits.lean | 8 ++-- Mathlib/FieldTheory/AbelRuffini.lean | 2 +- Mathlib/FieldTheory/Finite/Basic.lean | 2 +- Mathlib/FieldTheory/Fixed.lean | 2 +- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 2 +- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean | 2 +- Mathlib/FieldTheory/IsSepClosed.lean | 2 +- Mathlib/FieldTheory/Normal.lean | 4 +- Mathlib/FieldTheory/Separable.lean | 2 +- .../SplittingField/Construction.lean | 2 +- Mathlib/LinearAlgebra/Charpoly/Basic.lean | 2 +- Mathlib/LinearAlgebra/Matrix/Adjugate.lean | 2 +- Mathlib/LinearAlgebra/SModEq.lean | 18 +++++---- Mathlib/MeasureTheory/Function/Jacobian.lean | 4 +- .../Integral/CircleIntegral.lean | 2 +- .../Integral/IntervalIntegral.lean | 22 +++++----- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 6 +-- .../Cyclotomic/PrimitiveRoots.lean | 12 +++--- Mathlib/NumberTheory/FunctionField.lean | 12 ++++-- Mathlib/NumberTheory/Liouville/Basic.lean | 4 +- Mathlib/NumberTheory/PrimesCongruentOne.lean | 5 ++- Mathlib/Probability/Kernel/Invariance.lean | 8 ++-- Mathlib/RingTheory/Discriminant.lean | 12 +++--- Mathlib/RingTheory/Henselian.lean | 2 +- .../Polynomial/Cyclotomic/Basic.lean | 4 +- .../Polynomial/Cyclotomic/Expand.lean | 17 ++++---- .../Polynomial/Cyclotomic/Roots.lean | 4 +- .../Polynomial/Eisenstein/Basic.lean | 4 +- Mathlib/RingTheory/Polynomial/Pochhammer.lean | 4 +- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean | 2 +- .../WittVector/FrobeniusFractionField.lean | 3 +- Mathlib/SetTheory/ZFC/Basic.lean | 10 +++-- Mathlib/Topology/Sober.lean | 18 +++++---- 51 files changed, 203 insertions(+), 165 deletions(-) diff --git a/Archive/Imo/Imo2006Q5.lean b/Archive/Imo/Imo2006Q5.lean index cdad4cb7d10195..eec2993e00a828 100644 --- a/Archive/Imo/Imo2006Q5.lean +++ b/Archive/Imo/Imo2006Q5.lean @@ -150,8 +150,9 @@ 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.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 + 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] + at hab set b := P.eval a -- More auxiliary lemmas on degrees. have hPab : (P + (X : ℤ[X]) - a - b).natDegree = P.natDegree := by @@ -175,9 +176,9 @@ 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.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] + 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, + 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 -- the other. @@ -200,7 +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.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] + 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, + sub_eq_zero] exact Polynomial.isPeriodicPt_eval_two ⟨k, hk, ht⟩ #align imo2006_q5 imo2006_q5 diff --git a/Mathlib/Algebra/LinearRecurrence.lean b/Mathlib/Algebra/LinearRecurrence.lean index d417e8f1fb6044..a126ff53dfa62c 100644 --- a/Mathlib/Algebra/LinearRecurrence.lean +++ b/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.def, Polynomial.eval] + rw [charPoly, Polynomial.IsRoot.definition, Polynomial.eval] simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial, Polynomial.eval₂_sub] constructor diff --git a/Mathlib/Analysis/Asymptotics/Asymptotics.lean b/Mathlib/Analysis/Asymptotics/Asymptotics.lean index 9ced5a255ac8c6..fde3f60f3cc99a 100644 --- a/Mathlib/Analysis/Asymptotics/Asymptotics.lean +++ b/Mathlib/Analysis/Asymptotics/Asymptotics.lean @@ -191,16 +191,18 @@ 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 -theorem IsLittleO.def (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := +-- 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‖ := isLittleO_iff.1 h hc -#align asymptotics.is_o.def Asymptotics.IsLittleO.def +#align asymptotics.is_o.def Asymptotics.IsLittleO.definition 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.def zero_lt_one + simpa using h.definition zero_lt_one end Defs @@ -278,7 +280,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.def one_pos).mono fun x h₀' => _ + · refine' (H.definition 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₀' diff --git a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean index 49f0fa2ad5e60e..a58bf84da0181b 100644 --- a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean +++ b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean @@ -242,8 +242,8 @@ theorem hasIntegral_GP_pderiv (f : (Fin (n + 1) → ℝ) → E) /- At a point `x ∉ s`, we unfold the definition of Fréchet differentiability, then use 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.def ε'0) - with ⟨δ, δ0, Hδ⟩ + rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 + ((Hd x hx).isLittleO.definition ε'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 _ diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean index e2f2d956b77f52..d76b30450565cf 100644 --- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean +++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean @@ -77,7 +77,7 @@ theorem approximates_deriv_on_nhds {f : E → F} {f' : E →L[𝕜] F} {a : E} cases' hc with hE hc · refine' ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => _⟩ simp [@Subsingleton.elim E hE x y] - have := hf.def hc + have := hf.definition hc rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this rcases this with ⟨s, has, hs⟩ exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩ diff --git a/Mathlib/Analysis/Calculus/Rademacher.lean b/Mathlib/Analysis/Calculus/Rademacher.lean index b6c3a0361df58c..f7254b8116d81a 100644 --- a/Mathlib/Analysis/Calculus/Rademacher.lean +++ b/Mathlib/Analysis/Calculus/Rademacher.lean @@ -270,7 +270,7 @@ theorem hasFderivAt_of_hasLineDerivAt_of_closure {f : E → F} exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this have I : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_) - apply Asymptotics.IsLittleO.def ?_ δpos + apply Asymptotics.IsLittleO.definition ?_ δpos exact hasLineDerivAt_iff_isLittleO_nhds_zero.1 (hL v (hqs hv)) obtain ⟨r, r_pos, hr⟩ : ∃ (r : ℝ), 0 < r ∧ ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by diff --git a/Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean b/Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean index e0c04f9671b288..5c7bf66d83a6d3 100644 --- a/Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean +++ b/Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean @@ -90,7 +90,7 @@ theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux _ = ‖∫ x in Ι c d, deriv f x‖ := norm_integral_eq_norm_integral_Ioc _ _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := norm_integral_le_integral_norm _ _ ≤ ∫ x in Ι c d, C * ‖g x‖ := - set_integral_mono_on hfi.norm.def (hgi.mono_set hsub') measurableSet_uIoc hg + set_integral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg _ ≤ ∫ x in k, C * ‖g x‖ := by apply set_integral_mono_set hgi (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index 81a5c9a6eb2ca5..e0a882b8f5d3a5 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -172,7 +172,7 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) : -- Add 7 and 8 using 2 → 8 → 7 → 3 tfae_have 2 → 8 · rintro ⟨a, ha, H⟩ - refine' ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ _⟩ + refine' ⟨a, ha, (H.definition zero_lt_one).mono fun n hn ↦ _⟩ rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn tfae_have 8 → 7 exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩ diff --git a/Mathlib/CategoryTheory/Generator.lean b/Mathlib/CategoryTheory/Generator.lean index 78f0273a7ea570..42d6c64e2a9230 100644 --- a/Mathlib/CategoryTheory/Generator.lean +++ b/Mathlib/CategoryTheory/Generator.lean @@ -460,10 +460,12 @@ theorem isSeparator_def (G : C) : fun hG X Y f g hfg => hG _ _ fun h => hfg _ (Set.mem_singleton _) _⟩ #align category_theory.is_separator_def CategoryTheory.isSeparator_def -theorem IsSeparator.def {G : C} : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `IsSeparator.def`. +theorem IsSeparator.def' {G : C} : IsSeparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → f = g := (isSeparator_def _).1 -#align category_theory.is_separator.def CategoryTheory.IsSeparator.def +#align category_theory.is_separator.def CategoryTheory.IsSeparator.def' theorem isCoseparator_def (G : C) : IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g := @@ -474,10 +476,12 @@ theorem isCoseparator_def (G : C) : fun hG X Y f g hfg => hG _ _ fun h => hfg _ (Set.mem_singleton _) _⟩ #align category_theory.is_coseparator_def CategoryTheory.isCoseparator_def -theorem IsCoseparator.def {G : C} : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `IsCoseparator.def`. +theorem IsCoseparator.def' {G : C} : IsCoseparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g := (isCoseparator_def _).1 -#align category_theory.is_coseparator.def CategoryTheory.IsCoseparator.def +#align category_theory.is_coseparator.def CategoryTheory.IsCoseparator.def' theorem isDetector_def (G : C) : IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f := @@ -488,10 +492,12 @@ theorem isDetector_def (G : C) : fun hG X Y f hf => hG _ fun h => hf _ (Set.mem_singleton _) _⟩ #align category_theory.is_detector_def CategoryTheory.isDetector_def -theorem IsDetector.def {G : C} : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `IsDetector.def`. +theorem IsDetector.def' {G : C} : IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f := (isDetector_def _).1 -#align category_theory.is_detector.def CategoryTheory.IsDetector.def +#align category_theory.is_detector.def CategoryTheory.IsDetector.def' theorem isCodetector_def (G : C) : IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f := @@ -502,19 +508,21 @@ theorem isCodetector_def (G : C) : fun hG X Y f hf => hG _ fun h => hf _ (Set.mem_singleton _) _⟩ #align category_theory.is_codetector_def CategoryTheory.isCodetector_def -theorem IsCodetector.def {G : C} : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `IsCodetector.def`. +theorem IsCodetector.def' {G : C} : IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f := (isCodetector_def _).1 -#align category_theory.is_codetector.def CategoryTheory.IsCodetector.def +#align category_theory.is_codetector.def CategoryTheory.IsCodetector.def' theorem isSeparator_iff_faithful_coyoneda_obj (G : C) : IsSeparator G ↔ Faithful (coyoneda.obj (op G)) := - ⟨fun hG => ⟨fun hfg => hG.def _ _ (congr_fun hfg)⟩, fun _ => + ⟨fun hG => ⟨fun hfg => hG.def' _ _ (congr_fun hfg)⟩, fun _ => (isSeparator_def _).2 fun _ _ _ _ hfg => (coyoneda.obj (op G)).map_injective (funext hfg)⟩ #align category_theory.is_separator_iff_faithful_coyoneda_obj CategoryTheory.isSeparator_iff_faithful_coyoneda_obj theorem isCoseparator_iff_faithful_yoneda_obj (G : C) : IsCoseparator G ↔ Faithful (yoneda.obj G) := - ⟨fun hG => ⟨fun hfg => Quiver.Hom.unop_inj (hG.def _ _ (congr_fun hfg))⟩, fun _ => + ⟨fun hG => ⟨fun hfg => Quiver.Hom.unop_inj (hG.def' _ _ (congr_fun hfg))⟩, fun _ => (isCoseparator_def _).2 fun _ _ _ _ hfg => Quiver.Hom.op_inj <| (yoneda.obj G).map_injective (funext hfg)⟩ #align category_theory.is_coseparator_iff_faithful_yoneda_obj CategoryTheory.isCoseparator_iff_faithful_yoneda_obj @@ -548,7 +556,7 @@ theorem isSeparator_coprod (G H : C) [HasBinaryCoproduct G H] : refine' ⟨fun h X Y u v huv => _, fun h => (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩ - · refine' h.def _ _ fun g => coprod.hom_ext _ _ + · refine' h.def' _ _ fun g => coprod.hom_ext _ _ · simpa using huv G (by simp) (coprod.inl ≫ g) · simpa using huv H (by simp) (coprod.inr ≫ g) · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ @@ -572,7 +580,7 @@ theorem isSeparator_sigma {β : Type w} (f : β → C) [HasCoproduct f] : refine' ⟨fun h X Y u v huv => _, fun h => (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩ - · refine' h.def _ _ fun g => colimit.hom_ext fun b => _ + · refine' h.def' _ _ fun g => colimit.hom_ext fun b => _ simpa using huv (f b.as) (by simp) (colimit.ι (Discrete.functor f) _ ≫ g) · obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ classical simpa using Sigma.ι f b ≫= huv (Sigma.desc (Pi.single b g)) @@ -588,7 +596,7 @@ theorem isCoseparator_prod (G H : C) [HasBinaryProduct G H] : refine' ⟨fun h X Y u v huv => _, fun h => (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩ - · refine' h.def _ _ fun g => prod.hom_ext _ _ + · refine' h.def' _ _ fun g => prod.hom_ext _ _ · simpa using huv G (by simp) (g ≫ Limits.prod.fst) · simpa using huv H (by simp) (g ≫ Limits.prod.snd) · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ @@ -612,7 +620,7 @@ theorem isCoseparator_pi {β : Type w} (f : β → C) [HasProduct f] : refine' ⟨fun h X Y u v huv => _, fun h => (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩ - · refine' h.def _ _ fun g => limit.hom_ext fun b => _ + · refine' h.def' _ _ fun g => limit.hom_ext fun b => _ simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _) · obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b @@ -628,7 +636,7 @@ end ZeroMorphisms theorem isDetector_iff_reflectsIsomorphisms_coyoneda_obj (G : C) : IsDetector G ↔ ReflectsIsomorphisms (coyoneda.obj (op G)) := by refine' - ⟨fun hG => ⟨fun f hf => hG.def _ fun h => _⟩, fun h => + ⟨fun hG => ⟨fun f hf => hG.def' _ fun h => _⟩, fun h => (isDetector_def _).2 fun X Y f hf => _⟩ · rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf exact hf h @@ -640,7 +648,7 @@ theorem isDetector_iff_reflectsIsomorphisms_coyoneda_obj (G : C) : theorem isCodetector_iff_reflectsIsomorphisms_yoneda_obj (G : C) : IsCodetector G ↔ ReflectsIsomorphisms (yoneda.obj G) := by refine' ⟨fun hG => ⟨fun f hf => _⟩, fun h => (isCodetector_def _).2 fun X Y f hf => _⟩ - · refine' (isIso_unop_iff _).1 (hG.def _ _) + · refine' (isIso_unop_iff _).1 (hG.def' _ _) rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf · rw [← isIso_op_iff] suffices IsIso ((yoneda.obj G).map f.op) by diff --git a/Mathlib/CategoryTheory/Preadditive/Generator.lean b/Mathlib/CategoryTheory/Preadditive/Generator.lean index 1a8a07ecdc80c5..5331a28d607338 100644 --- a/Mathlib/CategoryTheory/Preadditive/Generator.lean +++ b/Mathlib/CategoryTheory/Preadditive/Generator.lean @@ -39,14 +39,14 @@ theorem Preadditive.isCoseparating_iff (𝒢 : Set C) : theorem Preadditive.isSeparator_iff (G : C) : IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = 0) → f = 0 := - ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [Limits.comp_zero] using hf), fun hG => + ⟨fun hG X Y f hf => hG.def' _ _ (by simpa only [Limits.comp_zero] using hf), fun hG => (isSeparator_def _).2 fun X Y f g hfg => sub_eq_zero.1 <| hG _ (by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg)⟩ #align category_theory.preadditive.is_separator_iff CategoryTheory.Preadditive.isSeparator_iff theorem Preadditive.isCoseparator_iff (G : C) : IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = 0) → f = 0 := - ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [Limits.zero_comp] using hf), fun hG => + ⟨fun hG X Y f hf => hG.def' _ _ (by simpa only [Limits.zero_comp] using hf), fun hG => (isCoseparator_def _).2 fun X Y f g hfg => sub_eq_zero.1 <| hG _ (by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg)⟩ #align category_theory.preadditive.is_coseparator_iff CategoryTheory.Preadditive.isCoseparator_iff diff --git a/Mathlib/CategoryTheory/Subterminal.lean b/Mathlib/CategoryTheory/Subterminal.lean index 2922c13a303928..34634e496e52a8 100644 --- a/Mathlib/CategoryTheory/Subterminal.lean +++ b/Mathlib/CategoryTheory/Subterminal.lean @@ -45,9 +45,11 @@ def IsSubterminal (A : C) : Prop := ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g #align category_theory.is_subterminal CategoryTheory.IsSubterminal -theorem IsSubterminal.def : IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g := +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `IsSubterminal.def`. +theorem IsSubterminal.def' : IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g := Iff.rfl -#align category_theory.is_subterminal.def CategoryTheory.IsSubterminal.def +#align category_theory.is_subterminal.def CategoryTheory.IsSubterminal.def' /-- If `A` is subterminal, the unique morphism from it to a terminal object is a monomorphism. The converse of `isSubterminal_of_mono_isTerminal_from`. @@ -97,7 +99,7 @@ The converse of `isSubterminal_of_isIso_diag`. theorem IsSubterminal.isIso_diag (hA : IsSubterminal A) [HasBinaryProduct A A] : IsIso (diag A) := ⟨⟨Limits.prod.fst, ⟨by simp, by - rw [IsSubterminal.def] at hA + rw [IsSubterminal.def'] at hA aesop_cat⟩⟩⟩ #align category_theory.is_subterminal.is_iso_diag CategoryTheory.IsSubterminal.isIso_diag diff --git a/Mathlib/Data/Polynomial/Degree/Definitions.lean b/Mathlib/Data/Polynomial/Degree/Definitions.lean index b00888e10a5a4d..7bed0dbbb3ca3d 100644 --- a/Mathlib/Data/Polynomial/Degree/Definitions.lean +++ b/Mathlib/Data/Polynomial/Degree/Definitions.lean @@ -85,9 +85,11 @@ theorem monic_of_subsingleton [Subsingleton R] (p : R[X]) : Monic p := Subsingleton.elim _ _ #align polynomial.monic_of_subsingleton Polynomial.monic_of_subsingleton -theorem Monic.def : Monic p ↔ leadingCoeff p = 1 := +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `Monic.def`. +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 @@ -1202,7 +1204,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 := diff --git a/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean b/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean index b354dd927c4ecb..9c421517e5dbdb 100644 --- a/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean +++ b/Mathlib/Data/Polynomial/Degree/TrailingDegree.lean @@ -67,9 +67,11 @@ def TrailingMonic (p : R[X]) := trailingCoeff p = (1 : R) #align polynomial.trailing_monic Polynomial.TrailingMonic -theorem TrailingMonic.def : TrailingMonic p ↔ trailingCoeff p = 1 := +-- 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 := Iff.rfl -#align polynomial.trailing_monic.def Polynomial.TrailingMonic.def +#align polynomial.trailing_monic.def Polynomial.TrailingMonic.definition instance TrailingMonic.decidable [DecidableEq R] : Decidable (TrailingMonic p) := inferInstanceAs <| Decidable (trailingCoeff p = (1 : R)) diff --git a/Mathlib/Data/Polynomial/Div.lean b/Mathlib/Data/Polynomial/Div.lean index b1a1d888d2d449..6a395402dc3943 100644 --- a/Mathlib/Data/Polynomial/Div.lean +++ b/Mathlib/Data/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 dvd_iff_modByMonic_eq_zero (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)⟩ @@ -605,7 +605,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.def, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul], + rw [← h, IsRoot.definition, 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)] @@ -684,7 +684,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.def, ← dvd_iff_isRoot] + rw [Ne.def, ← IsRoot.definition, ← 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 diff --git a/Mathlib/Data/Polynomial/Eval.lean b/Mathlib/Data/Polynomial/Eval.lean index eb1191d00aa781..47312862303f69 100644 --- a/Mathlib/Data/Polynomial/Eval.lean +++ b/Mathlib/Data/Polynomial/Eval.lean @@ -498,10 +498,12 @@ 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.def : IsRoot p a ↔ p.eval a = 0 := +theorem IsRoot.definition : IsRoot p a ↔ p.eval a = 0 := Iff.rfl -#align polynomial.is_root.def Polynomial.IsRoot.def +#align polynomial.is_root.def Polynomial.IsRoot.definition theorem IsRoot.eq_zero (h : IsRoot p x) : eval x p = 0 := h @@ -1158,11 +1160,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.def.1 H, mul_zero] + rw [IsRoot, eval_mul, IsRoot.definition.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.def.1 H, zero_mul] + by rw [IsRoot, eval_mul, IsRoot.definition.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) : @@ -1321,7 +1323,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.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm] + rw [IsRoot.definition, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm] #align polynomial.root_X_sub_C Polynomial.root_X_sub_C @[simp] diff --git a/Mathlib/Data/Polynomial/FieldDivision.lean b/Mathlib/Data/Polynomial/FieldDivision.lean index 65ec752c0e0063..dc891508b9f9d5 100644 --- a/Mathlib/Data/Polynomial/FieldDivision.lean +++ b/Mathlib/Data/Polynomial/FieldDivision.lean @@ -312,12 +312,13 @@ theorem mod_def : p % q = p %ₘ (q * C (leadingCoeff q)⁻¹) := rfl #align polynomial.mod_def Polynomial.mod_def 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] + show p %ₘ q = p %ₘ (q * C (leadingCoeff q)⁻¹) by + 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) := diff --git a/Mathlib/Data/Polynomial/Monic.lean b/Mathlib/Data/Polynomial/Monic.lean index 067bc69d00a60b..1d4afccc2722a2 100644 --- a/Mathlib/Data/Polynomial/Monic.lean +++ b/Mathlib/Data/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] diff --git a/Mathlib/Data/Polynomial/RingDivision.lean b/Mathlib/Data/Polynomial/RingDivision.lean index 7b06ab5f751361..b7d36bd8f8613d 100644 --- a/Mathlib/Data/Polynomial/RingDivision.lean +++ b/Mathlib/Data/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.def, eval_mul, mul_eq_zero] + simp_rw [dvd_iff_isRoot, IsRoot.definition, 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.def, aeval_def, eval₂_eq_eval_map] + rw [mem_roots w, IsRoot.definition, 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.def, sub_ne_zero, eval_sub, sub_eq_zero, eval_C] + rw [mem_roots', IsRoot.definition, 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.def, eval_sub, eval_C, eval_pow, + rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.definition, 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.def, ← eval₂_eq_eval_map, aeval_def] + rw [mem_roots', IsRoot.definition, ← 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.def, forall_exists_index, hp, not_false_eq_true] + IsRoot.definition, forall_exists_index, hp, not_false_eq_true] rintro x rfl exact heval _ diff --git a/Mathlib/Data/Polynomial/Splits.lean b/Mathlib/Data/Polynomial/Splits.lean index 8b1aa43bd8f47b..71fb6c020d7179 100644 --- a/Mathlib/Data/Polynomial/Splits.lean +++ b/Mathlib/Data/Polynomial/Splits.lean @@ -233,10 +233,12 @@ theorem splits_iff (f : K[X]) : #align polynomial.splits_iff Polynomial.splits_iff /-- This lemma is for polynomials over a field. -/ -theorem Splits.def {i : K →+* L} {f : K[X]} (h : Splits i f) : +-- 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) : 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 := @@ -409,7 +411,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 diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean index 5af30dd6a1bf5e..aad0b35295f9a8 100644 --- a/Mathlib/FieldTheory/AbelRuffini.lean +++ b/Mathlib/FieldTheory/AbelRuffini.lean @@ -130,7 +130,7 @@ theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F) have hn''' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1 have mem_range : ∀ {c : (X ^ n - C a).SplittingField}, (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) := fun {c} hc => - RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (h.def.resolve_left hn''' + RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (h.def'.resolve_left hn''' (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c)) (minpoly.dvd F c (by rwa [map_id, AlgHom.map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))) apply isSolvable_of_comm diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean index 9fa9d13705277a..51233a09808827 100644 --- a/Mathlib/FieldTheory/Finite/Basic.lean +++ b/Mathlib/FieldTheory/Finite/Basic.lean @@ -363,7 +363,7 @@ theorem roots_X_pow_card_sub_X : roots (X ^ q - X : K[X]) = Finset.univ.val := b have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ := by rw [eq_univ_iff_forall] intro x - rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X, + rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.definition, eval_sub, eval_pow, eval_X, sub_eq_zero, pow_card] rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self] apply nodup_roots diff --git a/Mathlib/FieldTheory/Fixed.lean b/Mathlib/FieldTheory/Fixed.lean index 44065687b0fe61..b8224b001115e6 100644 --- a/Mathlib/FieldTheory/Fixed.lean +++ b/Mathlib/FieldTheory/Fixed.lean @@ -213,7 +213,7 @@ theorem of_eval₂ (f : Polynomial (FixedPoints.subfield G F)) Fintype.prod_dvd_of_coprime (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x) fun y => QuotientGroup.induction_on y fun g => _ - rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.def, MulAction.ofQuotientStabilizer_mk, + rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.definition, MulAction.ofQuotientStabilizer_mk, Polynomial.eval_smul', ← this, ← Subfield.toSubring_subtype_eq_subtype, ← IsInvariantSubring.coe_subtypeHom' G (FixedPoints.subfield G F).toSubring, h, ← MulSemiringActionHom.coe_polynomial, ← MulSemiringActionHom.map_smul, smul_polynomial, diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 65c5eb794b916e..d0eec434360a06 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -92,7 +92,7 @@ theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z exact ne_of_gt (WithBot.coe_lt_coe.2 hn) obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this · use z - simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz + simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.definition] at hz exact sub_eq_zero.1 hz #align is_alg_closed.exists_pow_nat_eq IsAlgClosed.exists_pow_nat_eq diff --git a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean index 40aa4b98914e2a..ebde3627872035 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean @@ -81,7 +81,7 @@ because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degre theorem subset_polynomial_aeval (a : A) (p : 𝕜[X]) : (eval · p) '' σ a ⊆ σ (aeval a p) := by rintro _ ⟨k, hk, rfl⟩ let q := C (eval k p) - p - have hroot : IsRoot q k := by simp only [q, eval_C, eval_sub, sub_self, IsRoot.def] + have hroot : IsRoot q k := by simp only [q, eval_C, eval_sub, sub_self, IsRoot.definition] rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by simp only [q, aeval_C, AlgHom.map_sub, sub_left_inj] diff --git a/Mathlib/FieldTheory/IsSepClosed.lean b/Mathlib/FieldTheory/IsSepClosed.lean index e7d1cbe393ecc7..c872375468906a 100644 --- a/Mathlib/FieldTheory/IsSepClosed.lean +++ b/Mathlib/FieldTheory/IsSepClosed.lean @@ -113,7 +113,7 @@ theorem exists_pow_nat_eq [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero (n : k) · exact ⟨0, by rw [hx, pow_eq_zero_iff hn'.ne']⟩ · obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx use z - simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz + simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.definition, sub_eq_zero] using hz theorem exists_eq_mul_self [IsSepClosed k] (x : k) [h2 : NeZero (2 : k)] : ∃ z, x = z * z := by rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩ diff --git a/Mathlib/FieldTheory/Normal.lean b/Mathlib/FieldTheory/Normal.lean index f5565b010e43ba..8b067ef4f702c5 100644 --- a/Mathlib/FieldTheory/Normal.lean +++ b/Mathlib/FieldTheory/Normal.lean @@ -83,7 +83,7 @@ theorem Normal.exists_isSplittingField [h : Normal F K] [FiniteDimensional F K] mt (Polynomial.map_eq_zero <| algebraMap F K).1 <| Finset.prod_ne_zero_iff.2 fun x _ => _).2 _) · exact minpoly.ne_zero (h.isIntegral (s x)) - rw [IsRoot.def, eval_map, ← aeval_def, AlgHom.map_prod] + rw [IsRoot.definition, eval_map, ← aeval_def, AlgHom.map_prod] exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _) #align normal.exists_is_splitting_field Normal.exists_isSplittingField @@ -229,7 +229,7 @@ def AlgHom.restrictNormalAux [h : Normal F E] : rw [← hx, ← hy] apply minpoly.mem_range_of_degree_eq_one E refine' - Or.resolve_left (h.splits z).def (minpoly.ne_zero (h.isIntegral z)) (minpoly.irreducible _) + Or.resolve_left (h.splits z).def' (minpoly.ne_zero (h.isIntegral z)) (minpoly.irreducible _) (minpoly.dvd E _ (by simp [aeval_algHom_apply])) simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom] suffices IsIntegral F _ by exact this.tower_top diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index 1b979c553a03fd..2b13f713b32da1 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -508,7 +508,7 @@ theorem eq_X_sub_C_of_separable_of_root_eq {x : F} {h : F[X]} (h_sep : h.Separab constructor · apply Finset.mem_mk.mpr · rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)] - rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root] + rw [IsRoot.definition, ← eval₂_eq_eval_map, eval₂_hom, h_root] exact RingHom.map_zero i · exact nodup_roots (Separable.map h_sep) · exact h_roots diff --git a/Mathlib/FieldTheory/SplittingField/Construction.lean b/Mathlib/FieldTheory/SplittingField/Construction.lean index 71b7a5bcd6ccb7..6b11e9d54ac32e 100644 --- a/Mathlib/FieldTheory/SplittingField/Construction.lean +++ b/Mathlib/FieldTheory/SplittingField/Construction.lean @@ -90,7 +90,7 @@ theorem X_sub_C_mul_removeFactor (f : K[X]) (hf : f.natDegree ≠ 0) : let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf apply (mul_divByMonic_eq_iff_isRoot (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr - rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul] + rw [IsRoot.definition, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul] set_option linter.uppercaseLean3 false in #align polynomial.X_sub_C_mul_remove_factor Polynomial.X_sub_C_mul_removeFactor diff --git a/Mathlib/LinearAlgebra/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Charpoly/Basic.lean index 40f385bfe7e7f7..68f4e76ef4b157 100644 --- a/Mathlib/LinearAlgebra/Charpoly/Basic.lean +++ b/Mathlib/LinearAlgebra/Charpoly/Basic.lean @@ -109,7 +109,7 @@ theorem minpoly_coeff_zero_of_injective (hf : Function.Injective f) : exact minpoly.ne_zero (isIntegral f) hP have hPmonic : P.Monic := by suffices (minpoly R f).Monic by - rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this + rwa [Monic.def', hP, mul_comm, leadingCoeff_mul_X, ← Monic.def'] at this exact minpoly.monic (isIntegral f) have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _ simp only [hP, mul_eq_comp, ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp, AlgHom.map_mul, diff --git a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean index fdfcab0dee617f..0625ffb222ecf3 100644 --- a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean +++ b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean @@ -510,7 +510,7 @@ theorem adjugate_mul_distrib (A B : Matrix n n α) : adjugate (A * B) = adjugate have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by intro M refine' Polynomial.Monic.isRegular _ - simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm] + simp only [g, Polynomial.Monic.def', ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm] rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ← adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate, RingHom.map_adjugate, f'_inv, f'_g_mul] diff --git a/Mathlib/LinearAlgebra/SModEq.lean b/Mathlib/LinearAlgebra/SModEq.lean index 508b8a7fd67c70..e66d438db89012 100644 --- a/Mathlib/LinearAlgebra/SModEq.lean +++ b/Mathlib/LinearAlgebra/SModEq.lean @@ -32,14 +32,16 @@ notation:50 x " ≡ " y " [SMOD " N "]" => SModEq N x y variable {U U₁ U₂} -protected theorem SModEq.def : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `SModEq.def`. +protected theorem SModEq.def' : x ≡ y [SMOD U] ↔ (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y := Iff.rfl -#align smodeq.def SModEq.def +#align smodeq.def SModEq.def' namespace SModEq -theorem sub_mem : x ≡ y [SMOD U] ↔ x - y ∈ U := by rw [SModEq.def, Submodule.Quotient.eq] +theorem sub_mem : x ≡ y [SMOD U] ↔ x - y ∈ U := by rw [SModEq.def', Submodule.Quotient.eq] #align smodeq.sub_mem SModEq.sub_mem @[simp] @@ -49,7 +51,7 @@ theorem top : x ≡ y [SMOD (⊤ : Submodule R M)] := @[simp] theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y := by - rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero] + rw [SModEq.def', Submodule.Quotient.eq, mem_bot, sub_eq_zero] #align smodeq.bot SModEq.bot @[mono] @@ -83,16 +85,16 @@ instance instTrans : Trans (SModEq U) (SModEq U) (SModEq U) where trans := trans theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] := by - rw [SModEq.def] at hxy₁ hxy₂ ⊢ + rw [SModEq.def'] at hxy₁ hxy₂ ⊢ simp_rw [Quotient.mk_add, hxy₁, hxy₂] #align smodeq.add SModEq.add theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] := by - rw [SModEq.def] at hxy ⊢ + rw [SModEq.def'] at hxy ⊢ simp_rw [Quotient.mk_smul, hxy] #align smodeq.smul SModEq.smul -theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def, Submodule.Quotient.eq, sub_zero] +theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def', Submodule.Quotient.eq, sub_zero] #align smodeq.zero SModEq.zero theorem map (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f] := @@ -106,7 +108,7 @@ theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) : f.eval x ≡ f.eval y [SMOD I] := by - rw [SModEq.def] at h ⊢ + rw [SModEq.def'] at h ⊢ show Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y) replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h] diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean index c3b8ad47f7dc3e..e8e823e58498ec 100644 --- a/Mathlib/MeasureTheory/Function/Jacobian.lean +++ b/Mathlib/MeasureTheory/Function/Jacobian.lean @@ -154,7 +154,7 @@ theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCou simpa only [sub_pos] using mem_ball_iff_norm.mp hz obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ), 0 < δ ∧ ball x δ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖} := - Metric.mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos) + Metric.mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.definition εpos) obtain ⟨n, hn⟩ : ∃ n, u n < δ := ((tendsto_order.1 u_lim).2 _ δpos).exists refine' ⟨n, ⟨z, zT⟩, ⟨xs, _⟩⟩ intro y hy @@ -493,7 +493,7 @@ theorem _root_.ApproximatesLinearOn.norm_fderiv_sub_le {A : E →L[ℝ] E} {δ : (measure_closedBall_pos μ z εpos).ne' obtain ⟨ρ, ρpos, hρ⟩ : ∃ ρ > 0, ball x ρ ∩ s ⊆ {y : E | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖} := - mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos) + mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.definition εpos) -- for small enough `r`, the rescaled ball `r • closedBall z ε` is included in the set where -- `f y - f x` is well approximated by `f' x (y - x)`. have B₂ : ∀ᶠ r in 𝓝[>] (0 : ℝ), {x} + r • closedBall z ε ⊆ ball x ρ := by diff --git a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean index 8545828e719152..1fd08b590896c2 100644 --- a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean @@ -587,7 +587,7 @@ theorem hasSum_two_pi_I_cauchyPowerSeries_integral {f : ℂ → E} {c : ℂ} {R refine' intervalIntegral.hasSum_integral_of_dominated_convergence (fun n θ => ‖f (circleMap c R θ)‖ * (abs w / R) ^ n) (fun n => _) (fun n => _) _ _ _ · simp only [deriv_circleMap] - apply_rules [AEStronglyMeasurable.smul, hf.def.1] <;> apply Measurable.aestronglyMeasurable + apply_rules [AEStronglyMeasurable.smul, hf.def'.1] <;> apply Measurable.aestronglyMeasurable -- Porting note: these were `measurability` · exact (measurable_circleMap 0 R).mul_const I · exact (((measurable_circleMap c R).sub measurable_const).const_div w).pow measurable_const diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean index 60742260bf80a9..e0010a42c6377a 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean @@ -86,9 +86,9 @@ theorem intervalIntegrable_iff : IntervalIntegrable f μ a b ↔ IntegrableOn f /-- If a function is interval integrable with respect to a given measure `μ` on `a..b` then it is integrable on `uIoc a b` with respect to `μ`. -/ -theorem IntervalIntegrable.def (h : IntervalIntegrable f μ a b) : IntegrableOn f (Ι a b) μ := +theorem IntervalIntegrable.def' (h : IntervalIntegrable f μ a b) : IntegrableOn f (Ι a b) μ := intervalIntegrable_iff.mp h -#align interval_integrable.def IntervalIntegrable.def +#align interval_integrable.def IntervalIntegrable.def' theorem intervalIntegrable_iff_integrableOn_Ioc_of_le (hab : a ≤ b) : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ := by @@ -205,7 +205,7 @@ theorem abs {f : ℝ → ℝ} (h : IntervalIntegrable f μ a b) : theorem mono (hf : IntervalIntegrable f ν a b) (h1 : [[c, d]] ⊆ [[a, b]]) (h2 : μ ≤ ν) : IntervalIntegrable f μ c d := - intervalIntegrable_iff.mpr <| hf.def.mono (uIoc_subset_uIoc_of_uIcc_subset_uIcc h1) h2 + intervalIntegrable_iff.mpr <| hf.def'.mono (uIoc_subset_uIoc_of_uIcc_subset_uIcc h1) h2 #align interval_integrable.mono IntervalIntegrable.mono theorem mono_measure (hf : IntervalIntegrable f ν a b) (h : μ ≤ ν) : IntervalIntegrable f μ a b := @@ -219,7 +219,7 @@ theorem mono_set (hf : IntervalIntegrable f μ a b) (h : [[c, d]] ⊆ [[a, b]]) theorem mono_set_ae (hf : IntervalIntegrable f μ a b) (h : Ι c d ≤ᵐ[μ] Ι a b) : IntervalIntegrable f μ c d := - intervalIntegrable_iff.mpr <| hf.def.mono_set_ae h + intervalIntegrable_iff.mpr <| hf.def'.mono_set_ae h #align interval_integrable.mono_set_ae IntervalIntegrable.mono_set_ae theorem mono_set' (hf : IntervalIntegrable f μ a b) (hsub : Ι c d ⊆ Ι a b) : @@ -230,13 +230,13 @@ theorem mono_set' (hf : IntervalIntegrable f μ a b) (hsub : Ι c d ⊆ Ι a b) theorem mono_fun [NormedAddCommGroup F] {g : ℝ → F} (hf : IntervalIntegrable f μ a b) (hgm : AEStronglyMeasurable g (μ.restrict (Ι a b))) (hle : (fun x => ‖g x‖) ≤ᵐ[μ.restrict (Ι a b)] fun x => ‖f x‖) : IntervalIntegrable g μ a b := - intervalIntegrable_iff.2 <| hf.def.integrable.mono hgm hle + intervalIntegrable_iff.2 <| hf.def'.integrable.mono hgm hle #align interval_integrable.mono_fun IntervalIntegrable.mono_fun theorem mono_fun' {g : ℝ → ℝ} (hg : IntervalIntegrable g μ a b) (hfm : AEStronglyMeasurable f (μ.restrict (Ι a b))) (hle : (fun x => ‖f x‖) ≤ᵐ[μ.restrict (Ι a b)] g) : IntervalIntegrable f μ a b := - intervalIntegrable_iff.2 <| hg.def.integrable.mono' hfm hle + intervalIntegrable_iff.2 <| hg.def'.integrable.mono' hfm hle #align interval_integrable.mono_fun' IntervalIntegrable.mono_fun' protected theorem aestronglyMeasurable (h : IntervalIntegrable f μ a b) : @@ -581,7 +581,7 @@ nonrec theorem norm_integral_le_of_norm_le {g : ℝ → ℝ} (h : ∀ᵐ t ∂μ (hbound : IntervalIntegrable g μ a b) : ‖∫ t in a..b, f t ∂μ‖ ≤ |∫ t in a..b, g t ∂μ| := by simp_rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq, abs_eq_self.mpr (integral_nonneg_of_ae <| h.mono fun _t ht => (norm_nonneg _).trans ht), - norm_integral_le_of_norm_le hbound.def h] + norm_integral_le_of_norm_le hbound.def' h] #align interval_integral.norm_integral_le_of_norm_le intervalIntegral.norm_integral_le_of_norm_le theorem norm_integral_le_of_norm_le_const_ae {a b C : ℝ} {f : ℝ → E} @@ -600,13 +600,13 @@ theorem norm_integral_le_of_norm_le_const {a b C : ℝ} {f : ℝ → E} (h : ∀ @[simp] nonrec theorem integral_add (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) : ∫ x in a..b, f x + g x ∂μ = (∫ x in a..b, f x ∂μ) + ∫ x in a..b, g x ∂μ := by - simp only [intervalIntegral_eq_integral_uIoc, integral_add hf.def hg.def, smul_add] + simp only [intervalIntegral_eq_integral_uIoc, integral_add hf.def' hg.def', smul_add] #align interval_integral.integral_add intervalIntegral.integral_add nonrec theorem integral_finset_sum {ι} {s : Finset ι} {f : ι → ℝ → E} (h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) : ∫ x in a..b, ∑ i in s, f i x ∂μ = ∑ i in s, ∫ x in a..b, f i x ∂μ := by - simp only [intervalIntegral_eq_integral_uIoc, integral_finset_sum s fun i hi => (h i hi).def, + simp only [intervalIntegral_eq_integral_uIoc, integral_finset_sum s fun i hi => (h i hi).def', Finset.smul_sum] #align interval_integral.integral_finset_sum intervalIntegral.integral_finset_sum @@ -690,7 +690,7 @@ open ContinuousLinearMap theorem _root_.ContinuousLinearMap.intervalIntegral_apply {a b : ℝ} {φ : ℝ → F →L[𝕜] E} (hφ : IntervalIntegrable φ μ a b) (v : F) : (∫ x in a..b, φ x ∂μ) v = ∫ x in a..b, φ x v ∂μ := by - simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def v, coe_smul', Pi.smul_apply] + simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply] #align continuous_linear_map.interval_integral_apply ContinuousLinearMap.intervalIntegral_apply variable [NormedSpace ℝ F] [CompleteSpace F] @@ -1206,7 +1206,7 @@ theorem abs_integral_mono_interval {c d} (h : Ι a b ⊆ Ι c d) (hf : 0 ≤ᵐ[ calc |∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| := abs_integral_eq_abs_integral_uIoc f _ = ∫ x in Ι a b, f x ∂μ := (abs_of_nonneg (MeasureTheory.integral_nonneg_of_ae hf')) - _ ≤ ∫ x in Ι c d, f x ∂μ := (set_integral_mono_set hfi.def hf h.eventuallyLE) + _ ≤ ∫ x in Ι c d, f x ∂μ := (set_integral_mono_set hfi.def' hf h.eventuallyLE) _ ≤ |∫ x in Ι c d, f x ∂μ| := (le_abs_self _) _ = |∫ x in c..d, f x ∂μ| := (abs_integral_eq_abs_integral_uIoc f).symm #align interval_integral.abs_integral_mono_interval intervalIntegral.abs_integral_mono_interval diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 1e60e7c7965aea..f7a9e0474dba41 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -375,7 +375,7 @@ theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] rw [isRoot_of_unity_iff n.pos] refine' ⟨n, Nat.mem_divisors_self n n.ne_zero, _⟩ - rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def] + rw [IsRoot.definition, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def] exact hx.2 · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos @@ -545,7 +545,7 @@ instance isCyclotomicExtension [NeZero ((n : ℕ) : K)] : obtain ⟨ζ, hζ⟩ := exists_root_of_splits (algebraMap K (CyclotomicField n K)) (SplittingField.splits _) (degree_cyclotomic_pos n K n.pos).ne' - rw [← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ + rw [← eval_map, ← IsRoot.definition, map_cyclotomic, isRoot_cyclotomic_iff] at hζ -- Porting note: the first `?_` was `forall_eq.2 ⟨ζ, hζ⟩` that now fails. refine ⟨?_, ?_⟩ · simp only [mem_singleton_iff, forall_eq] @@ -731,7 +731,7 @@ theorem IsAlgClosed.isCyclotomicExtension (h : ∀ a ∈ S, NeZero ((a : ℕ) : obtain ⟨r, hr⟩ := IsAlgClosed.exists_aeval_eq_zero K _ (degree_cyclotomic_pos a K a.pos).ne' refine' ⟨r, _⟩ haveI := h a ha - rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr + rwa [coe_aeval_eq_eval, ← IsRoot.definition, isRoot_cyclotomic_iff] at hr #align is_alg_closed.is_cyclotomic_extension IsAlgClosed.isCyclotomicExtension instance IsAlgClosedOfCharZero.isCyclotomicExtension [CharZero K] : diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index 79176faebb064c..794a31f8f18122 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -91,13 +91,13 @@ theorem zeta_spec : IsPrimitiveRoot (zeta n A B) n := theorem aeval_zeta [IsDomain B] [NeZero ((n : ℕ) : B)] : aeval (zeta n A B) (cyclotomic n A) = 0 := by - rw [aeval_def, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] + rw [aeval_def, ← eval_map, ← IsRoot.definition, map_cyclotomic, isRoot_cyclotomic_iff] exact zeta_spec n A B #align is_cyclotomic_extension.aeval_zeta IsCyclotomicExtension.aeval_zeta theorem zeta_isRoot [IsDomain B] [NeZero ((n : ℕ) : B)] : IsRoot (cyclotomic n B) (zeta n A B) := by convert aeval_zeta n A B using 0 - rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic] + rw [IsRoot.definition, aeval_def, eval₂_eq_eval_map, map_cyclotomic] #align is_cyclotomic_extension.zeta_is_root IsCyclotomicExtension.zeta_isRoot theorem zeta_pow : zeta n A B ^ (n : ℕ) = 1 := @@ -151,16 +151,16 @@ noncomputable def embeddingsEquivPrimitiveRoots (C : Type*) [CommRing C] [IsDoma haveI hn := NeZero.of_noZeroSMulDivisors K C n refine' ⟨x.1, _⟩ cases x - rwa [mem_primitiveRoots n.pos, ← isRoot_cyclotomic_iff, IsRoot.def, ← - map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr, ← - eval₂_eq_eval_map, ← aeval_def] + rwa [mem_primitiveRoots n.pos, ← isRoot_cyclotomic_iff, IsRoot.definition, + ← map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr, + ← eval₂_eq_eval_map, ← aeval_def] invFun := fun x => by haveI := IsCyclotomicExtension.neZero' n K L haveI hn := NeZero.of_noZeroSMulDivisors K C n refine' ⟨x.1, _⟩ cases x rwa [aeval_def, eval₂_eq_eval_map, hζ.powerBasis_gen K, ← - hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_cyclotomic, ← IsRoot.def, + hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_cyclotomic, ← IsRoot.definition, isRoot_cyclotomic_iff, ← mem_primitiveRoots n.pos] left_inv := fun x => Subtype.ext rfl right_inv := fun x => Subtype.ext rfl } diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index 4d00f9ae67ca25..d6d65645258e58 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -244,11 +244,13 @@ def inftyValuedFqt : Valued (RatFunc Fq) ℤₘ₀ := set_option linter.uppercaseLean3 false in #align function_field.infty_valued_Fqt FunctionField.inftyValuedFqt -theorem inftyValuedFqt.def {x : RatFunc Fq} : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `inftyValuedFqt.def`. +theorem inftyValuedFqt.def' {x : RatFunc Fq} : @Valued.v (RatFunc Fq) _ _ _ (inftyValuedFqt Fq) x = inftyValuationDef Fq x := rfl set_option linter.uppercaseLean3 false in -#align function_field.infty_valued_Fqt.def FunctionField.inftyValuedFqt.def +#align function_field.infty_valued_Fqt.def FunctionField.inftyValuedFqt.def' /-- The completion `Fq((t⁻¹))` of `Fq(t)` with respect to the valuation at infinity. -/ def FqtInfty := @@ -269,11 +271,13 @@ instance valuedFqtInfty : Valued (FqtInfty Fq) ℤₘ₀ := set_option linter.uppercaseLean3 false in #align function_field.valued_Fqt_infty FunctionField.valuedFqtInfty -theorem valuedFqtInfty.def {x : FqtInfty Fq} : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `valuedFqtInfty.def`. +theorem valuedFqtInfty.def' {x : FqtInfty Fq} : Valued.v x = @Valued.extension (RatFunc Fq) _ _ _ (inftyValuedFqt Fq) x := rfl set_option linter.uppercaseLean3 false in -#align function_field.valued_Fqt_infty.def FunctionField.valuedFqtInfty.def +#align function_field.valued_Fqt_infty.def FunctionField.valuedFqtInfty.def' end InftyValuation diff --git a/Mathlib/NumberTheory/Liouville/Basic.lean b/Mathlib/NumberTheory/Liouville/Basic.lean index 6b05bc4aac1c4c..8fc003f401ca44 100644 --- a/Mathlib/NumberTheory/Liouville/Basic.lean +++ b/Mathlib/NumberTheory/Liouville/Basic.lean @@ -132,7 +132,7 @@ theorem exists_pos_real_of_irrational_root {α : ℝ} (ha : Irrational α) {f : (fR0.trans (Polynomial.map_zero _).symm) -- reformulating assumption `fa`: `α` is a root of `fR`. have ar : α ∈ (fR.roots.toFinset : Set ℝ) := - Finset.mem_coe.mpr (Multiset.mem_toFinset.mpr ((mem_roots fR0).mpr (IsRoot.def.mpr fa))) + Finset.mem_coe.mpr (Multiset.mem_toFinset.mpr ((mem_roots fR0).mpr (IsRoot.definition.mpr fa))) -- Since the polynomial `fR` has finitely many roots, there is a closed interval centered at `α` -- such that `α` is the only root of `fR` in the interval. obtain ⟨ζ, z0, U⟩ : ∃ ζ > 0, closedBall α ζ ∩ fR.roots.toFinset = {α} := @@ -170,7 +170,7 @@ theorem exists_pos_real_of_irrational_root {α : ℝ} (ha : Irrational α) {f : refine' (irrational_iff_ne_rational α).mp ha z (a + 1) (mem_singleton_iff.mp _).symm refine' U.subset _ refine' ⟨hq, Finset.mem_coe.mp (Multiset.mem_toFinset.mpr _)⟩ - exact (mem_roots fR0).mpr (IsRoot.def.mpr hy) + exact (mem_roots fR0).mpr (IsRoot.definition.mpr hy) #align liouville.exists_pos_real_of_irrational_root Liouville.exists_pos_real_of_irrational_root /-- **Liouville's Theorem** -/ diff --git a/Mathlib/NumberTheory/PrimesCongruentOne.lean b/Mathlib/NumberTheory/PrimesCongruentOne.lean index 240d877f150342..a33efa57527459 100644 --- a/Mathlib/NumberTheory/PrimesCongruentOne.lean +++ b/Mathlib/NumberTheory/PrimesCongruentOne.lean @@ -40,8 +40,9 @@ theorem exists_prime_gt_modEq_one {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) : haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩ have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) := by have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp - rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, ← Int.cast_ofNat, - this, eval₂_hom, Int.coe_castRingHom, ZMod.int_cast_zmod_eq_zero_iff_dvd _ _] + rw [IsRoot.definition, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom, + ← Int.cast_ofNat, this, eval₂_hom, Int.coe_castRingHom, + ZMod.int_cast_zmod_eq_zero_iff_dvd _ _] apply Int.dvd_natAbs.1 exact mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs have hpb : ¬p ∣ b := diff --git a/Mathlib/Probability/Kernel/Invariance.lean b/Mathlib/Probability/Kernel/Invariance.lean index e326ca7f0aa9e5..412a1a1c574fa0 100644 --- a/Mathlib/Probability/Kernel/Invariance.lean +++ b/Mathlib/Probability/Kernel/Invariance.lean @@ -76,12 +76,14 @@ def Invariant (κ : kernel α α) (μ : Measure α) : Prop := variable {κ η : kernel α α} {μ : Measure α} -theorem Invariant.def (hκ : Invariant κ μ) : μ.bind κ = μ := +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `Invariant.def`. +theorem Invariant.def' (hκ : Invariant κ μ) : μ.bind κ = μ := hκ -#align probability_theory.kernel.invariant.def ProbabilityTheory.kernel.Invariant.def +#align probability_theory.kernel.invariant.def ProbabilityTheory.kernel.Invariant.def' theorem Invariant.comp_const (hκ : Invariant κ μ) : κ ∘ₖ const α μ = const α μ := by - rw [← const_bind_eq_comp_const κ μ, hκ.def] + rw [← const_bind_eq_comp_const κ μ, hκ.def'] #align probability_theory.kernel.invariant.comp_const ProbabilityTheory.kernel.Invariant.comp_const theorem Invariant.comp [IsSFiniteKernel κ] (hκ : Invariant κ μ) (hη : Invariant η μ) : diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean index 9b401bf71b8598..56ec1493227ff1 100644 --- a/Mathlib/RingTheory/Discriminant.lean +++ b/Mathlib/RingTheory/Discriminant.lean @@ -224,7 +224,7 @@ theorem discr_powerBasis_eq_norm [IsSeparable K L] : nodup_roots (Separable.map (IsSeparable.separable K pb.gen)) have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ (minpoly K pb.gen).aroots E := by intro σ - rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply] + rw [mem_roots, IsRoot.definition, eval_map, ← aeval_def, aeval_algHom_apply] repeat' simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)] apply (algebraMap K E).injective rw [RingHom.map_mul, RingHom.map_pow, RingHom.map_neg, RingHom.map_one, @@ -243,11 +243,11 @@ theorem discr_powerBasis_eq_norm [IsSeparable K L] : refine prod_bij' (fun i _ ↦ ⟨e i.2, e i.1 pb.gen⟩) (fun σ hσ ↦ ⟨e.symm (PowerBasis.lift pb σ.2 ?_), e.symm σ.1⟩) ?_ ?_ ?_ ?_ (fun i _ ↦ by simp) -- Porting note: `@mem_compl` was not necessary. - <;> simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def, mem_roots', - minpoly.ne_zero (IsSeparable.isIntegral K pb.gen), not_false_eq_true, mem_singleton, true_and, - @mem_compl _ _ _ (_), Sigma.forall, Equiv.apply_symm_apply, PowerBasis.lift_gen, and_imp, - implies_true, forall_const, Equiv.symm_apply_apply, Sigma.ext_iff, Equiv.symm_apply_eq, - heq_eq_eq, and_true] at * + <;> simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.definition, + mem_roots', minpoly.ne_zero (IsSeparable.isIntegral K pb.gen), not_false_eq_true, + mem_singleton, true_and, @mem_compl _ _ _ (_), Sigma.forall, Equiv.apply_symm_apply, + PowerBasis.lift_gen, and_imp, implies_true, forall_const, Equiv.symm_apply_apply, + Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at * · simpa only [aeval_def, eval₂_eq_eval_map] using hσ.2.2 · exact fun a b hba ↦ ⟨fun h ↦ hba <| e.injective <| pb.algHom_ext h.symm, hroots _⟩ · rintro a b hba ha diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean index 523895f924d75a..0b68e7b3425605 100644 --- a/Mathlib/RingTheory/Henselian.lean +++ b/Mathlib/RingTheory/Henselian.lean @@ -204,7 +204,7 @@ instance (priority := 100) IsAdicComplete.henselianRing (R : Type*) [CommRing R] haveI := isLocalRingHom_of_le_jacobson_bot I (IsAdicComplete.le_jacobson_bot I) apply isUnit_of_map_unit (Ideal.Quotient.mk I) convert h₂ using 1 - exact SModEq.def.mp ((hc_mod n).eval _) + exact SModEq.def'.mp ((hc_mod n).eval _) have hfcI : ∀ n, f.eval (c n) ∈ I ^ (n + 1) := by intro n induction' n with n ih diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean index e56406a0d49ca9..eca166cd3b87e9 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean @@ -619,7 +619,7 @@ theorem coprime_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : rw [hprime.1.coprime_iff_not_dvd] intro h replace h := (ZMod.nat_cast_zmod_eq_zero_iff_dvd a p).2 h - rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot + rw [IsRoot.definition, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot by_cases hone : n = 1 · simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero, one_ne_zero, coeff_sub] at hroot @@ -642,7 +642,7 @@ theorem orderOf_root_cyclotomic_dvd {n : ℕ} (hpos : 0 < n) {p : ℕ} [Fact p.P simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow apply Units.val_eq_one.1 simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val] - rw [IsRoot.def] at hroot + rw [IsRoot.definition] at hroot rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons, eval_mul, hroot, zero_mul] #align polynomial.order_of_root_cyclotomic_dvd Polynomial.orderOf_root_cyclotomic_dvd diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean index ada0a5724c077f..6a2cc1a3b2ed41 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean @@ -55,14 +55,14 @@ theorem cyclotomic_expand_eq_cyclotomic_mul {p n : ℕ} (hp : Nat.Prime p) (hdiv have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne' rw [cyclotomic_eq_minpoly_rat hprim hpos] refine' minpoly.dvd ℚ _ _ - rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, + rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.definition, @isRoot_cyclotomic_iff] convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n) rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)] · have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm rw [cyclotomic_eq_minpoly_rat hprim hnpos] refine' minpoly.dvd ℚ _ _ - rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.def, ← + rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.definition, ← cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, @isRoot_cyclotomic_iff] exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv · rw [natDegree_expand, natDegree_cyclotomic, @@ -88,7 +88,7 @@ theorem cyclotomic_expand_eq_cyclotomic {p n : ℕ} (hp : Nat.Prime p) (hdiv : p have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm rw [cyclotomic_eq_minpoly hprim hpos] refine' minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) _ - rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, + rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.definition, @isRoot_cyclotomic_iff] · convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n) rw [Nat.mul_div_cancel _ hp.pos] @@ -169,12 +169,13 @@ theorem isRoot_cyclotomic_prime_pow_mul_iff_of_charP {m k p : ℕ} {R : Type*} [ rcases k.eq_zero_or_pos with (rfl | hk) · rw [pow_zero, one_mul, isRoot_cyclotomic_iff] refine' ⟨fun h => _, fun h => _⟩ - · rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow] at h + · rw [IsRoot.definition, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow] + at h replace h := pow_eq_zero h - rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h - · rw [← isRoot_cyclotomic_iff, IsRoot.def] at h - rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow, h, - zero_pow] + rwa [← IsRoot.definition, isRoot_cyclotomic_iff] at h + · rw [← isRoot_cyclotomic_iff, IsRoot.definition] at h + rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.definition, eval_pow, + h, zero_pow] exact Nat.sub_ne_zero_of_lt $ pow_right_strictMono hp.out.one_lt $ Nat.pred_lt hk.ne' #align polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean index c6945a0e076d08..1a2870c771e915 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean @@ -170,7 +170,7 @@ theorem cyclotomic_injective [CharZero R] : Function.Injective fun n => cyclotom theorem _root_.IsPrimitiveRoot.minpoly_dvd_cyclotomic {n : ℕ} {K : Type*} [Field K] {μ : K} (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero K] : minpoly ℤ μ ∣ cyclotomic n ℤ := by apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) - simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos + simpa [aeval_def, eval₂_eq_eval_map, IsRoot.definition] using h.isRoot_cyclotomic hpos #align is_primitive_root.minpoly_dvd_cyclotomic IsPrimitiveRoot.minpoly_dvd_cyclotomic section minpoly @@ -182,7 +182,7 @@ theorem _root_.IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible {K : Type*} (h : Irreducible <| cyclotomic n K) [NeZero (n : K)] : cyclotomic n K = minpoly K μ := by haveI := NeZero.of_noZeroSMulDivisors K R n refine' minpoly.eq_of_irreducible_of_monic h _ (cyclotomic.monic n K) - rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff] + rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.definition, isRoot_cyclotomic_iff] #align is_primitive_root.minpoly_eq_cyclotomic_of_irreducible IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible /-- `cyclotomic n ℤ` is the minimal polynomial of a primitive `n`-th root of unity `μ`. -/ diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean index 21b12711a50b1f..84cabaf1fb7893 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean @@ -131,7 +131,7 @@ theorem pow_natDegree_le_of_root_of_monic_mem {x : R} (hroot : IsRoot f x) (hmo obtain ⟨k, hk⟩ := exists_add_of_le hi rw [hk, pow_add] suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this - rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one, + rw [IsRoot.definition, eval_eq_sum_range, Finset.range_add_one, Finset.sum_insert Finset.not_mem_range_self, Finset.sum_range, hmo.coeff_natDegree, one_mul] at * rw [eq_neg_of_add_eq_zero_left hroot, Ideal.neg_mem_iff] @@ -146,7 +146,7 @@ theorem pow_natDegree_le_of_aeval_zero_of_monic_mem_map {x : S} (hx : aeval x f obtain ⟨k, hk⟩ := exists_add_of_le hi rw [hk, pow_add] exact mul_mem_right _ _ this - rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx + rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.definition] at hx exact pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le #align polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_aeval_zero_of_monic_mem_map Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean index 659b3a5a4b7663..4181a557a6097a 100644 --- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean +++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean @@ -71,7 +71,7 @@ theorem monic_ascPochhammer (n : ℕ) [Nontrivial S] [NoZeroDivisors S] : induction' n with n hn · simp · have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1 - rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul, + rw [ascPochhammer_succ_left, Monic.def', leadingCoeff_mul, leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn, monic_X, one_mul, one_mul, this, one_pow] @@ -265,7 +265,7 @@ theorem monic_descPochhammer (n : ℕ) [Nontrivial R] [NoZeroDivisors R] : · simp · have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1 have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R) - rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X, + rw [descPochhammer_succ_left, Monic.def', leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X, one_mul, one_mul, h, one_pow] section diff --git a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean index b6b76e7aaede4a..aefdf95f814cc2 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean @@ -198,7 +198,7 @@ then the minimal polynomial of a primitive `n`-th root of unity `μ` has `μ ^ m` as root. -/ theorem pow_isRoot_minpoly {m : ℕ} (hcop : Nat.Coprime m n) : IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m) := by - simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map] + simp only [minpoly_eq_pow_coprime h hcop, IsRoot.definition, eval_map] exact minpoly.aeval ℤ (μ ^ m) #align is_primitive_root.pow_is_root_minpoly IsPrimitiveRoot.pow_isRoot_minpoly diff --git a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean index fbf7fe28056a94..a70399e9c9bd79 100644 --- a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean +++ b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean @@ -132,7 +132,8 @@ theorem succNthVal_spec' (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) have := succNthVal_spec p n a₁ a₂ bs ha₁ ha₂ simp only [Polynomial.map_add, Polynomial.eval_X, Polynomial.map_pow, Polynomial.eval_C, Polynomial.eval_pow, succNthDefiningPoly, Polynomial.eval_mul, Polynomial.eval_add, - Polynomial.eval_sub, Polynomial.map_mul, Polynomial.map_sub, Polynomial.IsRoot.def] at this + Polynomial.eval_sub, Polynomial.map_mul, Polynomial.map_sub, Polynomial.IsRoot.definition] + at this convert this using 1 ring #align witt_vector.recursion_main.succ_nth_val_spec' WittVector.RecursionMain.succNthVal_spec' diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean index f3079fb2decbb2..b19e07676353ba 100644 --- a/Mathlib/SetTheory/ZFC/Basic.lean +++ b/Mathlib/SetTheory/ZFC/Basic.lean @@ -1381,15 +1381,17 @@ theorem hereditarily_iff : Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditaril rw [← Hereditarily] #align Set.hereditarily_iff ZFSet.hereditarily_iff -alias ⟨Hereditarily.def, _⟩ := hereditarily_iff -#align Set.hereditarily.def ZFSet.Hereditarily.def +-- Adaptation note: nightly-2024-03-15 +-- This has been renamed to avoid the clash with the reserved name `Hereditarily.def`. +alias ⟨Hereditarily.def', _⟩ := hereditarily_iff +#align Set.hereditarily.def ZFSet.Hereditarily.def' theorem Hereditarily.self (h : x.Hereditarily p) : p x := - h.def.1 + h.def'.1 #align Set.hereditarily.self ZFSet.Hereditarily.self theorem Hereditarily.mem (h : x.Hereditarily p) (hy : y ∈ x) : y.Hereditarily p := - h.def.2 _ hy + h.def'.2 _ hy #align Set.hereditarily.mem ZFSet.Hereditarily.mem theorem Hereditarily.empty : Hereditarily p x → p ∅ := by diff --git a/Mathlib/Topology/Sober.lean b/Mathlib/Topology/Sober.lean index bf8ffdbabcb471..9078a1046d6e63 100644 --- a/Mathlib/Topology/Sober.lean +++ b/Mathlib/Topology/Sober.lean @@ -39,10 +39,12 @@ theorem isGenericPoint_def {x : α} {S : Set α} : IsGenericPoint x S ↔ closur Iff.rfl #align is_generic_point_def isGenericPoint_def -theorem IsGenericPoint.def {x : α} {S : Set α} (h : IsGenericPoint x S) : +-- Adaptation note: 2024-03-15 +-- Renamed to avoid the reserved name `IsGenericPoint.def`. +theorem IsGenericPoint.def' {x : α} {S : Set α} (h : IsGenericPoint x S) : closure ({x} : Set α) = S := h -#align is_generic_point.def IsGenericPoint.def +#align is_generic_point.def IsGenericPoint.def' theorem isGenericPoint_closure {x : α} : IsGenericPoint x (closure ({x} : Set α)) := refl _ @@ -69,11 +71,11 @@ protected theorem mem (h : IsGenericPoint x S) : x ∈ S := #align is_generic_point.mem IsGenericPoint.mem protected theorem isClosed (h : IsGenericPoint x S) : IsClosed S := - h.def ▸ isClosed_closure + h.def' ▸ isClosed_closure #align is_generic_point.is_closed IsGenericPoint.isClosed protected theorem isIrreducible (h : IsGenericPoint x S) : IsIrreducible S := - h.def ▸ isIrreducible_singleton.closure + h.def' ▸ isIrreducible_singleton.closure #align is_generic_point.is_irreducible IsGenericPoint.isIrreducible protected theorem inseparable (h : IsGenericPoint x S) (h' : IsGenericPoint y S) : @@ -94,12 +96,12 @@ theorem disjoint_iff (h : IsGenericPoint x S) (hU : IsOpen U) : Disjoint S U ↔ #align is_generic_point.disjoint_iff IsGenericPoint.disjoint_iff theorem mem_closed_set_iff (h : IsGenericPoint x S) (hZ : IsClosed Z) : x ∈ Z ↔ S ⊆ Z := by - rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff] + rw [← h.def', hZ.closure_subset_iff, singleton_subset_iff] #align is_generic_point.mem_closed_set_iff IsGenericPoint.mem_closed_set_iff protected theorem image (h : IsGenericPoint x S) {f : α → β} (hf : Continuous f) : IsGenericPoint (f x) (closure (f '' S)) := by - rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf] + rw [isGenericPoint_def, ← h.def', ← image_singleton, closure_image_closure hf] #align is_generic_point.image IsGenericPoint.image end IsGenericPoint @@ -187,7 +189,7 @@ theorem ClosedEmbedding.quasiSober {f : α → β} (hf : ClosedEmbedding f) [Qua obtain ⟨y, -, rfl⟩ := hx.mem use y apply image_injective.mpr hf.inj - rw [← hx.def, ← hf.closure_image_eq, image_singleton] + rw [← hx.def', ← hf.closure_image_eq, image_singleton] #align closed_embedding.quasi_sober ClosedEmbedding.quasiSober theorem OpenEmbedding.quasiSober {f : α → β} (hf : OpenEmbedding f) [QuasiSober β] : @@ -233,7 +235,7 @@ theorem quasiSober_of_open_cover (S : Set (Set α)) (hS : ∀ s : S, IsOpen (s : apply le_antisymm · apply h'.closure_subset_iff.mpr simpa using this - rw [← image_singleton, ← closure_image_closure continuous_subtype_val, H.genericPoint_spec.def] + rw [← image_singleton, ← closure_image_closure continuous_subtype_val, H.genericPoint_spec.def'] refine' (subset_closure_inter_of_isPreirreducible_of_isOpen h.2 (hS ⟨U, hU⟩) ⟨x, hx, hU'⟩).trans (closure_mono _) rw [inter_comm t, ← Subtype.image_preimage_coe]