Theorem: PowerBasis.rat_hom_ext (FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean)

State before:
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
Tactic:
convert DFunLike.ext_iff.mp (pb.algHom_ext (show f' pb.gen = g' pb.gen from h))
State after:
no goals