convert DFunLike.ext_iff.mp (pb.algHom_ext (show f' pb.gen = g' pb.gen from h))
S : Type u_1
S' : Type u_2
inst✝¹ : CommRing S
hS : Algebra ℚ S
inst✝ : Ring S'
hS' : Algebra ℚ S'
pb : PowerBasis ℚ S
f g : S →+* S'
h : f pb.gen = g pb.gen
f' : S →ₐ[ℚ] S' := f.toRatAlgHom
g' : S →ₐ[ℚ] S' := g.toRatAlgHom
⊢ ∀ (x : S), f x = g x
no goals