case H
R : Type u_2
S : Type u_3
T : Type ?u.54281
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type ?u.54584
B : Type ?u.54587
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.55009
inst✝² : Field K
S' : Type u_1
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : ↑f pb.gen = ↑g pb.gen
x : S
⊢ ↑f x = ↑g x
R : Type u_2
S : Type u_3
T : Type ?u.54281
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type ?u.54584
B : Type ?u.54587
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.55009
inst✝² : Field K
S' : Type u_1
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : ↑f pb.gen = ↑g pb.gen
⊢ f = g
ext x
case H.intro
R : Type u_2
S : Type u_3
T : Type ?u.54281
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type ?u.54584
B : Type ?u.54587
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.55009
inst✝² : Field K
S' : Type u_1
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : ↑f✝ pb.gen = ↑g pb.gen
f : R[X]
⊢ ↑f✝ (↑(aeval pb.gen) f) = ↑g (↑(aeval pb.gen) f)
case H
R : Type u_2
S : Type u_3
T : Type ?u.54281
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type ?u.54584
B : Type ?u.54587
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.55009
inst✝² : Field K
S' : Type u_1
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : ↑f pb.gen = ↑g pb.gen
x : S
⊢ ↑f x = ↑g x
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
no goals
case H.intro
R : Type u_2
S : Type u_3
T : Type ?u.54281
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type ?u.54584
B : Type ?u.54587
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra A B
K : Type ?u.55009
inst✝² : Field K
S' : Type u_1
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : ↑f✝ pb.gen = ↑g pb.gen
f : R[X]
⊢ ↑f✝ (↑(aeval pb.gen) f) = ↑g (↑(aeval pb.gen) f)
rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]