change

Author: mattrobball

Mathlib/Algebra/Algebra/Basic.lean

@@ -248,7 +248,6 @@ end FieldDivisionRing
 end algebraMap
 
 /-- Creating an algebra from a morphism to the center of a semiring. -/
-@[reducible]
 def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
     (h : ∀ c x, i c * x = x * i c) : Algebra R S where
   smul c x := i c * x
@@ -258,7 +257,6 @@ def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S)
 #align ring_hom.to_algebra' RingHom.toAlgebra'
 
 /-- Creating an algebra from a morphism to a commutative semiring. -/
-@[reducible]
 def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
   i.toAlgebra' fun _ => mul_comm _
 #align ring_hom.to_algebra RingHom.toAlgebra