bump to nightly-2023-04-06-10

mathlib commit leanprover-community/mathlib@06a655b

Mathbin/Analysis/LocallyConvex/AbsConvex.lean

@@ -167,9 +167,9 @@ variable [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
 variable [SMulCommClass ℝ 𝕜 E] [LocallyConvexSpace ℝ E]
 
 /-- The topology of a locally convex space is induced by the gauge seminorm family. -/
-theorem withGaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) :=
+theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) :=
   by
-  refine' SeminormFamily.withSeminormsOfHasBasis _ _
+  refine' SeminormFamily.withSeminorms_of_hasBasis _ _
   refine' (nhds_basis_abs_convex_open 𝕜 E).to_hasBasis (fun s hs => _) fun s hs => _
   · refine' ⟨s, ⟨_, rfl.subset⟩⟩
     convert(gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
@@ -189,5 +189,5 @@ theorem withGaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) :=
   have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
   rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
   exact S.coe_is_open.smul₀ hr''
-#align with_gauge_seminorm_family withGaugeSeminormFamily
+#align with_gauge_seminorm_family with_gaugeSeminormFamily
 

Mathbin/Analysis/LocallyConvex/WeakDual.lean

@@ -145,10 +145,10 @@ theorem LinearMap.hasBasis_weakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
   exact hx y hy
 #align linear_map.has_basis_weak_bilin LinearMap.hasBasis_weakBilin
 
-theorem LinearMap.weakBilinWithSeminorms (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
+theorem LinearMap.weakBilin_withSeminorms (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
     WithSeminorms (LinearMap.toSeminormFamily B : F → Seminorm 𝕜 (WeakBilin B)) :=
-  SeminormFamily.withSeminormsOfHasBasis _ B.hasBasis_weakBilin
-#align linear_map.weak_bilin_with_seminorms LinearMap.weakBilinWithSeminorms
+  SeminormFamily.withSeminorms_of_hasBasis _ B.hasBasis_weakBilin
+#align linear_map.weak_bilin_with_seminorms LinearMap.weakBilin_withSeminorms
 
 end Topology
 
@@ -159,7 +159,7 @@ variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [M
 variable [Nonempty ι] [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
 
 instance {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} : LocallyConvexSpace ℝ (WeakBilin B) :=
-  B.weakBilinWithSeminorms.toLocallyConvexSpace
+  B.weakBilin_withSeminorms.toLocallyConvexSpace
 
 end LocallyConvex
 

Mathbin/Analysis/LocallyConvex/WithSeminorms.lean

@@ -298,7 +298,7 @@ variable {p : SeminormFamily 𝕜 E ι}
 theorem WithSeminorms.topologicalAddGroup (hp : WithSeminorms p) : TopologicalAddGroup E :=
   by
   rw [hp.with_seminorms_eq]
-  exact AddGroupFilterBasis.is_topological_add_group _
+  exact AddGroupFilterBasis.isTopologicalAddGroup _
 #align with_seminorms.topological_add_group WithSeminorms.topologicalAddGroup
 
 theorem WithSeminorms.hasBasis (hp : WithSeminorms p) :
@@ -432,20 +432,20 @@ variable [Nonempty ι]
 
 include t
 
-theorem SeminormFamily.withSeminormsOfNhds (p : SeminormFamily 𝕜 E ι)
+theorem SeminormFamily.withSeminorms_of_nhds (p : SeminormFamily 𝕜 E ι)
     (h : 𝓝 (0 : E) = p.ModuleFilterBasis.toFilterBasis.filterₓ) : WithSeminorms p :=
   by
   refine'
     ⟨TopologicalAddGroup.ext inferInstance p.add_group_filter_basis.is_topological_add_group _⟩
   rw [AddGroupFilterBasis.nhds_zero_eq]
   exact h
-#align seminorm_family.with_seminorms_of_nhds SeminormFamily.withSeminormsOfNhds
+#align seminorm_family.with_seminorms_of_nhds SeminormFamily.withSeminorms_of_nhds
 
-theorem SeminormFamily.withSeminormsOfHasBasis (p : SeminormFamily 𝕜 E ι)
+theorem SeminormFamily.withSeminorms_of_hasBasis (p : SeminormFamily 𝕜 E ι)
     (h : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basis_sets) id) : WithSeminorms p :=
-  p.withSeminormsOfNhds <|
+  p.withSeminorms_of_nhds <|
     Filter.HasBasis.eq_of_same_basis h p.AddGroupFilterBasis.toFilterBasis.HasBasis
-#align seminorm_family.with_seminorms_of_has_basis SeminormFamily.withSeminormsOfHasBasis
+#align seminorm_family.with_seminorms_of_has_basis SeminormFamily.withSeminorms_of_hasBasis
 
 theorem SeminormFamily.withSeminorms_iff_nhds_eq_infᵢ (p : SeminormFamily 𝕜 E ι) :
     WithSeminorms p ↔ (𝓝 0 : Filter E) = ⨅ i, (𝓝 0).comap (p i) :=
@@ -505,7 +505,7 @@ end TopologicalAddGroup
 section NormedSpace
 
 /-- The topology of a `normed_space 𝕜 E` is induced by the seminorm `norm_seminorm 𝕜 E`. -/
-theorem normWithSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
+theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
     WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E :=
   by
   let p : SeminormFamily 𝕜 E (Fin 1) := fun _ => normSeminorm 𝕜 E
@@ -525,7 +525,7 @@ theorem normWithSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E]
   · rw [Finset.sup_const h]
   rw [finset.not_nonempty_iff_eq_empty.mp h, Finset.sup_empty, ball_bot _ hr]
   exact Set.subset_univ _
-#align norm_with_seminorms normWithSeminorms
+#align norm_with_seminorms norm_withSeminorms
 
 end NormedSpace
 
@@ -661,15 +661,15 @@ theorem cont_withSeminorms_normedSpace (F) [SeminormedAddCommGroup F] [NormedSpa
     (f : E →ₛₗ[τ₁₂] F) (hf : ∃ (s : Finset ι)(C : ℝ≥0), (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
     Continuous f := by
   rw [← Seminorm.isBounded_const (Fin 1)] at hf
-  exact continuous_from_bounded hp (normWithSeminorms 𝕝₂ F) f hf
+  exact continuous_from_bounded hp (norm_withSeminorms 𝕝₂ F) f hf
 #align seminorm.cont_with_seminorms_normed_space Seminorm.cont_withSeminorms_normedSpace
 
 theorem cont_normedSpace_to_withSeminorms (E) [SeminormedAddCommGroup E] [NormedSpace 𝕝 E]
     [UniformSpace F] [UniformAddGroup F] {q : ι → Seminorm 𝕝₂ F} (hq : WithSeminorms q)
     (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i : ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • normSeminorm 𝕝 E) :
     Continuous f := by
   rw [← Seminorm.const_isBounded (Fin 1)] at hf
-  exact continuous_from_bounded (normWithSeminorms 𝕝 E) hq f hf
+  exact continuous_from_bounded (norm_withSeminorms 𝕝 E) hq f hf
 #align seminorm.cont_normed_space_to_with_seminorms Seminorm.cont_normedSpace_to_withSeminorms
 
 end Seminorm
@@ -687,7 +687,7 @@ theorem WithSeminorms.toLocallyConvexSpace {p : SeminormFamily 𝕜 E ι} (hp :
     LocallyConvexSpace ℝ E :=
   by
   apply of_basis_zero ℝ E id fun s => s ∈ p.basis_sets
-  · rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.n_zero]
+  · rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
     exact FilterBasis.hasBasis _
   · intro s hs
     change s ∈ Set.unionᵢ _ at hs
@@ -706,7 +706,7 @@ variable (𝕜) [NormedField 𝕜] [NormedSpace ℝ 𝕜] [SeminormedAddCommGrou
 slightly weaker instance version. -/
 theorem NormedSpace.toLocallyConvexSpace' [NormedSpace 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] :
     LocallyConvexSpace ℝ E :=
-  (normWithSeminorms 𝕜 E).toLocallyConvexSpace
+  (norm_withSeminorms 𝕜 E).toLocallyConvexSpace
 #align normed_space.to_locally_convex_space' NormedSpace.toLocallyConvexSpace'
 
 /-- See `normed_space.to_locally_convex_space'` for a slightly stronger version which is not an
@@ -745,7 +745,7 @@ theorem SeminormFamily.finset_sup_comp (q : SeminormFamily 𝕜₂ F ι) (s : Fi
 
 variable [TopologicalSpace F] [TopologicalAddGroup F]
 
-theorem LinearMap.withSeminormsInduced [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι}
+theorem LinearMap.withSeminorms_induced [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι}
     (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) :
     @WithSeminorms 𝕜 E ι _ _ _ _ (q.comp f) (induced f inferInstance) :=
   by
@@ -755,7 +755,7 @@ theorem LinearMap.withSeminormsInduced [hι : Nonempty ι] {q : SeminormFamily 
     q.with_seminorms_iff_nhds_eq_infi.mp hq, Filter.comap_infᵢ]
   refine' infᵢ_congr fun i => _
   exact Filter.comap_comap
-#align linear_map.with_seminorms_induced LinearMap.withSeminormsInduced
+#align linear_map.with_seminorms_induced LinearMap.withSeminorms_induced
 
 theorem Inducing.withSeminorms [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q)
     [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : Inducing f) : WithSeminorms (q.comp f) :=

Mathbin/Analysis/SchwartzSpace.lean

@@ -504,23 +504,23 @@ theorem schwartzSeminormFamily_apply_zero :
 instance : TopologicalSpace 𝓢(E, F) :=
   (schwartzSeminormFamily ℝ E F).ModuleFilterBasis.topology'
 
-theorem schwartzWithSeminorms : WithSeminorms (schwartzSeminormFamily 𝕜 E F) :=
+theorem schwartz_withSeminorms : WithSeminorms (schwartzSeminormFamily 𝕜 E F) :=
   by
   have A : WithSeminorms (schwartzSeminormFamily ℝ E F) := ⟨rfl⟩
   rw [SeminormFamily.withSeminorms_iff_nhds_eq_infᵢ] at A⊢
   rw [A]
   rfl
-#align schwartz_with_seminorms schwartzWithSeminorms
+#align schwartz_with_seminorms schwartz_withSeminorms
 
 variable {𝕜 E F}
 
 instance : ContinuousSMul 𝕜 𝓢(E, F) :=
   by
-  rw [(schwartzWithSeminorms 𝕜 E F).withSeminorms_eq]
+  rw [(schwartz_withSeminorms 𝕜 E F).withSeminorms_eq]
   exact (schwartzSeminormFamily 𝕜 E F).ModuleFilterBasis.ContinuousSMul
 
 instance : TopologicalAddGroup 𝓢(E, F) :=
-  (schwartzSeminormFamily ℝ E F).AddGroupFilterBasis.is_topological_add_group
+  (schwartzSeminormFamily ℝ E F).AddGroupFilterBasis.isTopologicalAddGroup
 
 instance : UniformSpace 𝓢(E, F) :=
   (schwartzSeminormFamily ℝ E F).AddGroupFilterBasis.UniformSpace
@@ -529,10 +529,10 @@ instance : UniformAddGroup 𝓢(E, F) :=
   (schwartzSeminormFamily ℝ E F).AddGroupFilterBasis.UniformAddGroup
 
 instance : LocallyConvexSpace ℝ 𝓢(E, F) :=
-  (schwartzWithSeminorms ℝ E F).toLocallyConvexSpace
+  (schwartz_withSeminorms ℝ E F).toLocallyConvexSpace
 
 instance : TopologicalSpace.FirstCountableTopology 𝓢(E, F) :=
-  (schwartzWithSeminorms ℝ E F).first_countable
+  (schwartz_withSeminorms ℝ E F).first_countable
 
 end Topology
 
@@ -594,8 +594,8 @@ def mkClm [RingHomIsometric σ] (A : (D → E) → F → G)
   cont := by
     change Continuous (mk_lm A hadd hsmul hsmooth hbound : 𝓢(D, E) →ₛₗ[σ] 𝓢(F, G))
     refine'
-      Seminorm.continuous_from_bounded (schwartzWithSeminorms 𝕜 D E) (schwartzWithSeminorms 𝕜' F G)
-        _ fun n => _
+      Seminorm.continuous_from_bounded (schwartz_withSeminorms 𝕜 D E)
+        (schwartz_withSeminorms 𝕜' F G) _ fun n => _
     rcases hbound n with ⟨s, C, hC, h⟩
     refine' ⟨s, ⟨C, hC⟩, fun f => _⟩
     simp only [Seminorm.comp_apply, Seminorm.smul_apply, NNReal.smul_def, Algebra.id.smul_eq_mul,
@@ -686,8 +686,8 @@ def toBoundedContinuousFunctionClm : 𝓢(E, F) →L[𝕜] E →ᵇ F :=
     cont := by
       change Continuous (to_bounded_continuous_function_lm 𝕜 E F)
       refine'
-        Seminorm.continuous_from_bounded (schwartzWithSeminorms 𝕜 E F)
-          (normWithSeminorms 𝕜 (E →ᵇ F)) _ fun i => ⟨{0}, 1, fun f => _⟩
+        Seminorm.continuous_from_bounded (schwartz_withSeminorms 𝕜 E F)
+          (norm_withSeminorms 𝕜 (E →ᵇ F)) _ fun i => ⟨{0}, 1, fun f => _⟩
       rw [Finset.sup_singleton, one_smul, Seminorm.comp_apply, coe_normSeminorm,
         schwartz_seminorm_family_apply_zero, BoundedContinuousFunction.norm_le (map_nonneg _ _)]
       intro x

Mathbin/FieldTheory/KrullTopology.lean

@@ -211,7 +211,7 @@ instance krullTopology (K L : Type _) [Field K] [Field L] [Algebra K L] :
 
 /-- For a field extension `L/K`, the Krull topology on `L ≃ₐ[K] L` makes it a topological group. -/
 instance (K L : Type _) [Field K] [Field L] [Algebra K L] : TopologicalGroup (L ≃ₐ[K] L) :=
-  GroupFilterBasis.is_topologicalGroup (galGroupBasis K L)
+  GroupFilterBasis.isTopologicalGroup (galGroupBasis K L)
 
 section KrullT2