bump to nightly-2023-04-17-16

mathlib commit leanprover-community/mathlib@17ad94b

Mathbin/Analysis/Calculus/BumpFunctionFindim.lean

@@ -360,7 +360,7 @@ theorem w_integral {D : ℝ} (Dpos : 0 < D) : (∫ x : E, w D x ∂μ) = 1 :=
 theorem w_support {D : ℝ} (Dpos : 0 < D) : support (w D : E → ℝ) = ball 0 D :=
   by
   have B : D • ball (0 : E) 1 = ball 0 D := by
-    rw [smul_unit_ball Dpos.ne', Real.norm_of_nonneg Dpos.le]
+    rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]
   have C : D ^ finrank ℝ E ≠ 0 := pow_ne_zero _ Dpos.ne'
   simp only [W_def, Algebra.id.smul_eq_mul, support_mul, support_inv, univ_inter,
     support_comp_inv_smul₀ Dpos.ne', u_support, B, support_const (u_int_pos E).ne', support_const C,

Mathbin/Analysis/Convex/Gauge.lean

@@ -494,7 +494,7 @@ theorem gauge_unit_ball (x : E) : gauge (Metric.ball (0 : E) 1) x = ‖x‖ :=
 
 theorem gauge_ball (hr : 0 < r) (x : E) : gauge (Metric.ball (0 : E) r) x = ‖x‖ / r :=
   by
-  rw [← smul_unit_ball_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
+  rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
     abs_of_nonneg hr.le, div_eq_inv_mul]
   simp_rw [mem_ball_zero_iff, norm_neg]
   exact fun _ => id

Mathbin/Analysis/Convex/StrictConvexSpace.lean

@@ -93,7 +93,7 @@ variable [NormedSpace ℝ E]
 /-- A real normed vector space is strictly convex provided that the unit ball is strictly convex. -/
 theorem StrictConvexSpace.ofStrictConvexClosedUnitBall [LinearMap.CompatibleSMul E E 𝕜 ℝ]
     (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) : StrictConvexSpace 𝕜 E :=
-  ⟨fun r hr => by simpa only [smul_closed_unit_ball_of_nonneg hr.le] using h.smul r⟩
+  ⟨fun r hr => by simpa only [smul_closedUnitBall_of_nonneg hr.le] using h.smul r⟩
 #align strict_convex_space.of_strict_convex_closed_unit_ball StrictConvexSpace.ofStrictConvexClosedUnitBall
 
 /-- Strict convexity is equivalent to `‖a • x + b • y‖ < 1` for all `x` and `y` of norm at most `1`

Mathbin/CategoryTheory/Arrow.lean

@@ -164,14 +164,14 @@ theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) :
   sq.w
 #align category_theory.arrow.w_mk_right CategoryTheory.Arrow.w_mk_right
 
-#print CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right /-
-theorem isIso_of_iso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
+#print CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right /-
+theorem isIso_of_isIso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
     [IsIso ff.right] : IsIso ff :=
   {
     out :=
       ⟨⟨inv ff.left, inv ff.right⟩, by ext <;> dsimp <;> simp only [is_iso.hom_inv_id], by
         ext <;> dsimp <;> simp only [is_iso.inv_hom_id]⟩ }
-#align category_theory.arrow.is_iso_of_iso_left_of_is_iso_right CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right
+#align category_theory.arrow.is_iso_of_iso_left_of_is_iso_right CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right
 -/
 
 /- warning: category_theory.arrow.iso_mk -> CategoryTheory.Arrow.isoMk is a dubious translation:

Mathbin/Data/Zmod/Quotient.lean

@@ -193,7 +193,7 @@ variable {α : Type _} [Group α] (a : α)
 theorem order_eq_card_zpowers' : orderOf a = Nat.card (zpowers a) :=
   by
   have := Nat.card_congr (MulAction.orbitZpowersEquiv a (1 : α))
-  rwa [Nat.card_zMod, orbit_subgroup_one_eq_self, eq_comm] at this
+  rwa [Nat.card_zmod, orbit_subgroup_one_eq_self, eq_comm] at this
 #align order_eq_card_zpowers' order_eq_card_zpowers'
 #align add_order_eq_card_zmultiples' add_order_eq_card_zmultiples'
 

Mathbin/LinearAlgebra/Dimension.lean

@@ -1267,7 +1267,7 @@ variable (R)
 #print rank_self /-
 @[simp]
 theorem rank_self : Module.rank R R = 1 := by
-  rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_pUnit]
+  rw [← Cardinal.lift_inj, ← (Basis.singleton PUnit R).mk_eq_rank, Cardinal.mk_punit]
 #align rank_self rank_self
 -/
 

Mathbin/MeasureTheory/Constructions/Pi.lean

@@ -307,8 +307,8 @@ def pi' : Measure (∀ i, α i) :=
 
 theorem pi'_pi [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) : pi' μ (pi univ s) = ∏ i, μ i (s i) :=
   by
-  rw [pi', ← MeasurableEquiv.piMeasurableEquivTprod_symm_apply, MeasurableEquiv.map_apply,
-      MeasurableEquiv.piMeasurableEquivTprod_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
+  rw [pi', ← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
+      MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
       List.prod_toFinset, sorted_univ_to_finset] <;>
     exact sorted_univ_nodup ι
 #align measure_theory.measure.pi'_pi MeasureTheory.Measure.pi'_pi

Mathbin/MeasureTheory/Measure/HaarLebesgue.lean

@@ -533,7 +533,7 @@ theorem add_haar_closedBall_mul_of_pos (x : E) {r : ℝ} (hr : 0 < r) (s : ℝ)
     μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s) :=
   by
   have : closed_ball (0 : E) (r * s) = r • closed_ball 0 s := by
-    simp [smul_closed_ball' hr.ne' (0 : E), abs_of_nonneg hr.le]
+    simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]
   simp only [this, add_haar_smul, abs_of_nonneg hr.le, add_haar_closed_ball_center, abs_pow]
 #align measure_theory.measure.add_haar_closed_ball_mul_of_pos MeasureTheory.Measure.add_haar_closedBall_mul_of_pos
 

Mathbin/SetTheory/Cardinal/Basic.lean

@@ -575,16 +575,16 @@ theorem mk_option {α : Type u} : (#Option α) = (#α) + 1 :=
   (Equiv.optionEquivSumPUnit α).cardinal_eq
 #align cardinal.mk_option Cardinal.mk_option
 
-/- warning: cardinal.mk_psum -> Cardinal.mk_pSum is a dubious translation:
+/- warning: cardinal.mk_psum -> Cardinal.mk_psum is a dubious translation:
 lean 3 declaration is
   forall (α : Type.{u1}) (β : Type.{u2}), Eq.{succ (succ (max u1 u2))} Cardinal.{max u1 u2} (Cardinal.mk.{max u1 u2} (PSum.{succ u1, succ u2} α β)) (HAdd.hAdd.{succ (max u1 u2), succ (max u1 u2), succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.{max u1 u2} Cardinal.{max u1 u2} (instHAdd.{succ (max u1 u2)} Cardinal.{max u1 u2} Cardinal.hasAdd.{max u1 u2}) (Cardinal.lift.{u2, u1} (Cardinal.mk.{u1} α)) (Cardinal.lift.{u1, u2} (Cardinal.mk.{u2} β)))
 but is expected to have type
   forall (α : Type.{u1}) (β : Type.{u2}), Eq.{max (succ (succ u1)) (succ (succ u2))} Cardinal.{max u1 u2} (Cardinal.mk.{max u1 u2} (PSum.{succ u1, succ u2} α β)) (HAdd.hAdd.{max (succ u1) (succ u2), max (succ u1) (succ u2), max (succ u1) (succ u2)} Cardinal.{max u1 u2} Cardinal.{max u2 u1} Cardinal.{max u1 u2} (instHAdd.{max (succ u1) (succ u2)} Cardinal.{max u1 u2} Cardinal.instAddCardinal.{max u1 u2}) (Cardinal.lift.{u2, u1} (Cardinal.mk.{u1} α)) (Cardinal.lift.{u1, u2} (Cardinal.mk.{u2} β)))
-Case conversion may be inaccurate. Consider using '#align cardinal.mk_psum Cardinal.mk_pSumₓ'. -/
+Case conversion may be inaccurate. Consider using '#align cardinal.mk_psum Cardinal.mk_psumₓ'. -/
 @[simp]
-theorem mk_pSum (α : Type u) (β : Type v) : (#PSum α β) = lift.{v} (#α) + lift.{u} (#β) :=
+theorem mk_psum (α : Type u) (β : Type v) : (#PSum α β) = lift.{v} (#α) + lift.{u} (#β) :=
   (mk_congr (Equiv.psumEquivSum α β)).trans (mk_sum α β)
-#align cardinal.mk_psum Cardinal.mk_pSum
+#align cardinal.mk_psum Cardinal.mk_psum
 
 /- warning: cardinal.mk_fintype -> Cardinal.mk_fintype is a dubious translation:
 lean 3 declaration is
@@ -920,7 +920,7 @@ private theorem add_le_add' : ∀ {a b c d : Cardinal}, a ≤ b → c ≤ d →
 lean 3 declaration is
   CovariantClass.{succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} (HAdd.hAdd.{succ u1, succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} Cardinal.{u1} (instHAdd.{succ u1} Cardinal.{u1} Cardinal.hasAdd.{u1})) (LE.le.{succ u1} Cardinal.{u1} Cardinal.hasLe.{u1})
 but is expected to have type
-  CovariantClass.{succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5036 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5038 : Cardinal.{u1}) => HAdd.hAdd.{succ u1, succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} Cardinal.{u1} (instHAdd.{succ u1} Cardinal.{u1} Cardinal.instAddCardinal.{u1}) x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5036 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5038) (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5051 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5053 : Cardinal.{u1}) => LE.le.{succ u1} Cardinal.{u1} Cardinal.instLECardinal.{u1} x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5051 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5053)
+  CovariantClass.{succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5061 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5063 : Cardinal.{u1}) => HAdd.hAdd.{succ u1, succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} Cardinal.{u1} (instHAdd.{succ u1} Cardinal.{u1} Cardinal.instAddCardinal.{u1}) x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5061 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5063) (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5076 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5078 : Cardinal.{u1}) => LE.le.{succ u1} Cardinal.{u1} Cardinal.instLECardinal.{u1} x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5076 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5078)
 Case conversion may be inaccurate. Consider using '#align cardinal.add_covariant_class Cardinal.add_covariantClassₓ'. -/
 instance add_covariantClass : CovariantClass Cardinal Cardinal (· + ·) (· ≤ ·) :=
   ⟨fun a b c => add_le_add' le_rfl⟩
@@ -930,7 +930,7 @@ instance add_covariantClass : CovariantClass Cardinal Cardinal (· + ·) (· ≤
 lean 3 declaration is
   CovariantClass.{succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} (Function.swap.{succ (succ u1), succ (succ u1), succ (succ u1)} Cardinal.{u1} Cardinal.{u1} (fun (ᾰ : Cardinal.{u1}) (ᾰ : Cardinal.{u1}) => Cardinal.{u1}) (HAdd.hAdd.{succ u1, succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} Cardinal.{u1} (instHAdd.{succ u1} Cardinal.{u1} Cardinal.hasAdd.{u1}))) (LE.le.{succ u1} Cardinal.{u1} Cardinal.hasLe.{u1})
 but is expected to have type
-  CovariantClass.{succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} (Function.swap.{succ (succ u1), succ (succ u1), succ (succ u1)} Cardinal.{u1} Cardinal.{u1} (fun (ᾰ : Cardinal.{u1}) (ᾰ : Cardinal.{u1}) => Cardinal.{u1}) (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5103 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5105 : Cardinal.{u1}) => HAdd.hAdd.{succ u1, succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} Cardinal.{u1} (instHAdd.{succ u1} Cardinal.{u1} Cardinal.instAddCardinal.{u1}) x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5103 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5105)) (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5118 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5120 : Cardinal.{u1}) => LE.le.{succ u1} Cardinal.{u1} Cardinal.instLECardinal.{u1} x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5118 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5120)
+  CovariantClass.{succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} (Function.swap.{succ (succ u1), succ (succ u1), succ (succ u1)} Cardinal.{u1} Cardinal.{u1} (fun (ᾰ : Cardinal.{u1}) (ᾰ : Cardinal.{u1}) => Cardinal.{u1}) (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5128 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5130 : Cardinal.{u1}) => HAdd.hAdd.{succ u1, succ u1, succ u1} Cardinal.{u1} Cardinal.{u1} Cardinal.{u1} (instHAdd.{succ u1} Cardinal.{u1} Cardinal.instAddCardinal.{u1}) x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5128 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5130)) (fun (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5143 : Cardinal.{u1}) (x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5145 : Cardinal.{u1}) => LE.le.{succ u1} Cardinal.{u1} Cardinal.instLECardinal.{u1} x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5143 x._@.Mathlib.SetTheory.Cardinal.Basic._hyg.5145)
 Case conversion may be inaccurate. Consider using '#align cardinal.add_swap_covariant_class Cardinal.add_swap_covariantClassₓ'. -/
 instance add_swap_covariantClass : CovariantClass Cardinal Cardinal (swap (· + ·)) (· ≤ ·) :=
   ⟨fun a b c h => add_le_add' h le_rfl⟩
@@ -2909,23 +2909,23 @@ theorem mk_empty : (#Empty) = 0 :=
 #align cardinal.mk_empty Cardinal.mk_empty
 -/
 
-#print Cardinal.mk_pEmpty /-
+#print Cardinal.mk_pempty /-
 @[simp]
-theorem mk_pEmpty : (#PEmpty) = 0 :=
+theorem mk_pempty : (#PEmpty) = 0 :=
   mk_eq_zero _
-#align cardinal.mk_pempty Cardinal.mk_pEmpty
+#align cardinal.mk_pempty Cardinal.mk_pempty
 -/
 
-#print Cardinal.mk_pUnit /-
+#print Cardinal.mk_punit /-
 @[simp]
-theorem mk_pUnit : (#PUnit) = 1 :=
+theorem mk_punit : (#PUnit) = 1 :=
   mk_eq_one PUnit
-#align cardinal.mk_punit Cardinal.mk_pUnit
+#align cardinal.mk_punit Cardinal.mk_punit
 -/
 
 #print Cardinal.mk_unit /-
 theorem mk_unit : (#Unit) = 1 :=
-  mk_pUnit
+  mk_punit
 #align cardinal.mk_unit Cardinal.mk_unit
 -/
 
@@ -2936,18 +2936,18 @@ theorem mk_singleton {α : Type u} (x : α) : (#({x} : Set α)) = 1 :=
 #align cardinal.mk_singleton Cardinal.mk_singleton
 -/
 
-#print Cardinal.mk_pLift_true /-
+#print Cardinal.mk_plift_true /-
 @[simp]
-theorem mk_pLift_true : (#PLift True) = 1 :=
+theorem mk_plift_true : (#PLift True) = 1 :=
   mk_eq_one _
-#align cardinal.mk_plift_true Cardinal.mk_pLift_true
+#align cardinal.mk_plift_true Cardinal.mk_plift_true
 -/
 
-#print Cardinal.mk_pLift_false /-
+#print Cardinal.mk_plift_false /-
 @[simp]
-theorem mk_pLift_false : (#PLift False) = 0 :=
+theorem mk_plift_false : (#PLift False) = 0 :=
   mk_eq_zero _
-#align cardinal.mk_plift_false Cardinal.mk_pLift_false
+#align cardinal.mk_plift_false Cardinal.mk_plift_false
 -/
 
 #print Cardinal.mk_vector /-

Mathbin/SetTheory/Cardinal/Finite.lean

@@ -150,22 +150,22 @@ theorem card_prod (α β : Type _) : Nat.card (α × β) = Nat.card α * Nat.car
   simp only [Nat.card, mk_prod, to_nat_mul, to_nat_lift]
 #align nat.card_prod Nat.card_prod
 
-/- warning: nat.card_ulift -> Nat.card_uLift is a dubious translation:
+/- warning: nat.card_ulift -> Nat.card_ulift is a dubious translation:
 lean 3 declaration is
   forall (α : Type.{u1}), Eq.{1} Nat (Nat.card.{max u1 u2} (ULift.{u2, u1} α)) (Nat.card.{u1} α)
 but is expected to have type
   forall (α : Type.{u2}), Eq.{1} Nat (Nat.card.{max u2 u1} (ULift.{u1, u2} α)) (Nat.card.{u2} α)
-Case conversion may be inaccurate. Consider using '#align nat.card_ulift Nat.card_uLiftₓ'. -/
+Case conversion may be inaccurate. Consider using '#align nat.card_ulift Nat.card_uliftₓ'. -/
 @[simp]
-theorem card_uLift (α : Type _) : Nat.card (ULift α) = Nat.card α :=
+theorem card_ulift (α : Type _) : Nat.card (ULift α) = Nat.card α :=
   card_congr Equiv.ulift
-#align nat.card_ulift Nat.card_uLift
+#align nat.card_ulift Nat.card_ulift
 
-#print Nat.card_pLift /-
+#print Nat.card_plift /-
 @[simp]
-theorem card_pLift (α : Type _) : Nat.card (PLift α) = Nat.card α :=
+theorem card_plift (α : Type _) : Nat.card (PLift α) = Nat.card α :=
   card_congr Equiv.plift
-#align nat.card_plift Nat.card_pLift
+#align nat.card_plift Nat.card_plift
 -/
 
 #print Nat.card_pi /-
@@ -186,14 +186,14 @@ theorem card_fun [Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α
   rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
 #align nat.card_fun Nat.card_fun
 
-#print Nat.card_zMod /-
+#print Nat.card_zmod /-
 @[simp]
-theorem card_zMod (n : ℕ) : Nat.card (ZMod n) = n :=
+theorem card_zmod (n : ℕ) : Nat.card (ZMod n) = n :=
   by
   cases n
   · exact Nat.card_eq_zero_of_infinite
   · rw [Nat.card_eq_fintype_card, ZMod.card]
-#align nat.card_zmod Nat.card_zMod
+#align nat.card_zmod Nat.card_zmod
 -/
 
 end Nat

Mathbin/Topology/Algebra/Nonarchimedean/AdicTopology.lean

@@ -54,7 +54,7 @@ open Topology Pointwise
 
 namespace Ideal
 
-theorem adicBasis (I : Ideal R) : SubmodulesRingBasis fun n : ℕ => (I ^ n • ⊤ : Ideal R) :=
+theorem adic_basis (I : Ideal R) : SubmodulesRingBasis fun n : ℕ => (I ^ n • ⊤ : Ideal R) :=
   { inter := by
       suffices ∀ i j : ℕ, ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j by simpa
       intro i j
@@ -71,21 +71,21 @@ theorem adicBasis (I : Ideal R) : SubmodulesRingBasis fun n : ℕ => (I ^ n •
       use n
       rintro a ⟨x, b, hx, hb, rfl⟩
       exact (I ^ n).smul_mem x hb }
-#align ideal.adic_basis Ideal.adicBasis
+#align ideal.adic_basis Ideal.adic_basis
 
 /-- The adic ring filter basis associated to an ideal `I` is made of powers of `I`. -/
 def ringFilterBasis (I : Ideal R) :=
-  I.adicBasis.toRing_subgroups_basis.toRingFilterBasis
+  I.adic_basis.toRing_subgroups_basis.toRingFilterBasis
 #align ideal.ring_filter_basis Ideal.ringFilterBasis
 
 /-- The adic topology associated to an ideal `I`. This topology admits powers of `I` as a basis of
 neighborhoods of zero. It is compatible with the ring structure and is non-archimedean. -/
 def adicTopology (I : Ideal R) : TopologicalSpace R :=
-  (adicBasis I).topology
+  (adic_basis I).topology
 #align ideal.adic_topology Ideal.adicTopology
 
 theorem nonarchimedean (I : Ideal R) : @NonarchimedeanRing R _ I.adicTopology :=
-  I.adicBasis.toRing_subgroups_basis.nonarchimedean
+  I.adic_basis.toRing_subgroups_basis.nonarchimedean
 #align ideal.nonarchimedean Ideal.nonarchimedean
 
 /-- For the `I`-adic topology, the neighborhoods of zero has basis given by the powers of `I`. -/
@@ -114,7 +114,7 @@ theorem hasBasis_nhds_adic (I : Ideal R) (x : R) :
 
 variable (I : Ideal R) (M : Type _) [AddCommGroup M] [Module R M]
 
-theorem adicModuleBasis :
+theorem adic_module_basis :
     I.RingFilterBasis.SubmodulesBasis fun n : ℕ => I ^ n • (⊤ : Submodule R M) :=
   { inter := fun i j =>
       ⟨max i j,
@@ -126,13 +126,13 @@ theorem adicModuleBasis :
         by
         replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
         exact smul_mem_smul a_in mem_top⟩ }
-#align ideal.adic_module_basis Ideal.adicModuleBasis
+#align ideal.adic_module_basis Ideal.adic_module_basis
 
 /-- The topology on a `R`-module `M` associated to an ideal `M`. Submodules $I^n M$,
 written `I^n • ⊤` form a basis of neighborhoods of zero. -/
 def adicModuleTopology : TopologicalSpace M :=
-  @ModuleFilterBasis.topology R M _ I.adicBasis.topology _ _
-    (I.RingFilterBasis.ModuleFilterBasis (I.adicModuleBasis M))
+  @ModuleFilterBasis.topology R M _ I.adic_basis.topology _ _
+    (I.RingFilterBasis.ModuleFilterBasis (I.adic_module_basis M))
 #align ideal.adic_module_topology Ideal.adicModuleTopology
 
 /-- The elements of the basis of neighborhoods of zero for the `I`-adic topology
@@ -177,7 +177,7 @@ theorem isAdic_iff [top : TopologicalSpace R] [TopologicalRing R] {J : Ideal R}
     · apply @TopologicalRing.to_topologicalAddGroup
     · apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup
     · ext s
-      letI := Ideal.adicBasis J
+      letI := Ideal.adic_basis J
       rw [J.has_basis_nhds_zero_adic.mem_iff]
       constructor <;> intro H
       · rcases H₂ s H with ⟨n, h⟩