bump to nightly-2023-07-04-09

mathlib commit leanprover-community/mathlib@728ef9d
leanprover-community · Jul 4, 2023 · 8a4e8ca · 8a4e8ca
1 parent 0989637
commit 8a4e8ca
Show file tree

Hide file tree

Showing 6 changed files with 90 additions and 32 deletions.
diff --git a/Mathbin/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathbin/AlgebraicGeometry/PrimeSpectrum/Basic.lean
@@ -800,7 +800,7 @@ theorem comap_singleton_isClosed_of_isIntegral (f : R →+* S) (hf : f.IsIntegra
     (x : PrimeSpectrum S) (hx : IsClosed ({x} : Set (PrimeSpectrum S))) :
     IsClosed ({comap f x} : Set (PrimeSpectrum R)) :=
   (isClosed_singleton_iff_isMaximal _).2
-    (Ideal.isMaximal_comap_of_isIntegral_of_is_maximal' f hf x.asIdeal <|
+    (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' f hf x.asIdeal <|
       (isClosed_singleton_iff_isMaximal x).1 hx)
 #align prime_spectrum.comap_singleton_is_closed_of_is_integral PrimeSpectrum.comap_singleton_isClosed_of_isIntegral
 -/

diff --git a/Mathbin/RingTheory/Ideal/Over.lean b/Mathbin/RingTheory/Ideal/Over.lean
@@ -353,11 +353,11 @@ theorem isMaximal_comap_of_isIntegral_of_isMaximal (hRS : Algebra.IsIntegral R S
 #align ideal.is_maximal_comap_of_is_integral_of_is_maximal Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
 -/
 
-#print Ideal.isMaximal_comap_of_isIntegral_of_is_maximal' /-
-theorem isMaximal_comap_of_isIntegral_of_is_maximal' {R S : Type _} [CommRing R] [CommRing S]
+#print Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' /-
+theorem isMaximal_comap_of_isIntegral_of_isMaximal' {R S : Type _} [CommRing R] [CommRing S]
     (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) (hI : I.IsMaximal) : IsMaximal (I.comap f) :=
   @isMaximal_comap_of_isIntegral_of_isMaximal R _ S _ f.toAlgebra hf I hI
-#align ideal.is_maximal_comap_of_is_integral_of_is_maximal' Ideal.isMaximal_comap_of_isIntegral_of_is_maximal'
+#align ideal.is_maximal_comap_of_is_integral_of_is_maximal' Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'
 -/
 
 section IsIntegralClosure

diff --git a/Mathbin/RingTheory/IntegralClosure.lean b/Mathbin/RingTheory/IntegralClosure.lean
@@ -701,21 +701,21 @@ theorem integralClosure.isIntegral (x : integralClosure R A) : IsIntegral R x :=
 #align integral_closure.is_integral integralClosure.isIntegral
 -/
 
-#print RingHom.is_integral_of_is_integral_mul_unit /-
-theorem RingHom.is_integral_of_is_integral_mul_unit (x y : S) (r : R) (hr : f r * y = 1)
+#print RingHom.isIntegral_of_isIntegral_mul_unit /-
+theorem RingHom.isIntegral_of_isIntegral_mul_unit (x y : S) (r : R) (hr : f r * y = 1)
     (hx : f.IsIntegralElem (x * y)) : f.IsIntegralElem x :=
   by
   obtain ⟨p, ⟨p_monic, hp⟩⟩ := hx
   refine' ⟨scale_roots p r, ⟨(monic_scale_roots_iff r).2 p_monic, _⟩⟩
   convert scale_roots_eval₂_eq_zero f hp
   rw [mul_comm x y, ← mul_assoc, hr, one_mul]
-#align ring_hom.is_integral_of_is_integral_mul_unit RingHom.is_integral_of_is_integral_mul_unit
+#align ring_hom.is_integral_of_is_integral_mul_unit RingHom.isIntegral_of_isIntegral_mul_unit
 -/
 
 #print isIntegral_of_isIntegral_mul_unit /-
 theorem isIntegral_of_isIntegral_mul_unit {x y : A} {r : R} (hr : algebraMap R A r * y = 1)
     (hx : IsIntegral R (x * y)) : IsIntegral R x :=
-  (algebraMap R A).is_integral_of_is_integral_mul_unit x y r hr hx
+  (algebraMap R A).isIntegral_of_isIntegral_mul_unit x y r hr hx
 #align is_integral_of_is_integral_mul_unit isIntegral_of_isIntegral_mul_unit
 -/
 
@@ -728,11 +728,11 @@ theorem isIntegral_of_mem_closure' (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x
 #align is_integral_of_mem_closure' isIntegral_of_mem_closure'
 -/
 
-#print is_integral_of_mem_closure'' /-
-theorem is_integral_of_mem_closure'' {S : Type _} [CommRing S] {f : R →+* S} (G : Set S)
+#print isIntegral_of_mem_closure'' /-
+theorem isIntegral_of_mem_closure'' {S : Type _} [CommRing S] {f : R →+* S} (G : Set S)
     (hG : ∀ x ∈ G, f.IsIntegralElem x) : ∀ x ∈ Subring.closure G, f.IsIntegralElem x := fun x hx =>
   @isIntegral_of_mem_closure' R S _ _ f.toAlgebra G hG x hx
-#align is_integral_of_mem_closure'' is_integral_of_mem_closure''
+#align is_integral_of_mem_closure'' isIntegral_of_mem_closure''
 -/
 
 #print IsIntegral.pow /-