chore: rename IsScalarTower.of_ring_hom (#9330)

It's about `AlgHom` not `RingHom`. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
leanprover-community · Dec 30, 2023 · d8b7c07 · d8b7c07
1 parent 42060a2
commit d8b7c07
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean
@@ -175,12 +175,12 @@ instance (priority := 999) subsemiring (U : Subsemiring S) : IsScalarTower U S A
 #align is_scalar_tower.subsemiring IsScalarTower.subsemiring
 
 -- Porting note: @[nolint instance_priority]
-instance (priority := 999) of_ring_hom {R A B : Type*} [CommSemiring R] [CommSemiring A]
+instance (priority := 999) of_algHom {R A B : Type*} [CommSemiring R] [CommSemiring A]
     [CommSemiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
     @IsScalarTower R A B _ f.toRingHom.toAlgebra.toSMul _ :=
   letI := (f : A →+* B).toAlgebra
   of_algebraMap_eq fun x => (f.commutes x).symm
-#align is_scalar_tower.of_ring_hom IsScalarTower.of_ring_hom
+#align is_scalar_tower.of_ring_hom IsScalarTower.of_algHom
 
 end Semiring
 

diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
@@ -285,7 +285,7 @@ theorem equiv {C : Type*} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension
     (f : B ≃ₐ[A] C) : IsCyclotomicExtension S A C := by
   letI : Algebra B C := f.toAlgHom.toRingHom.toAlgebra
   haveI : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective
-  haveI : IsScalarTower A B C := IsScalarTower.of_ring_hom f.toAlgHom
+  haveI : IsScalarTower A B C := IsScalarTower.of_algHom f.toAlgHom
   exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)
 #align is_cyclotomic_extension.equiv IsCyclotomicExtension.equiv