case h
R : Type ?u.705600
S : Type u_2
T : Type ?u.705606
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_1
B : Type ?u.705912
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type ?u.706334
inst✝⁴ : Field K
S' : Type u_3
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
x : S
⊢ ↑(equivOfRoot pb (map pb e) h₁ h₂) x = ↑e x
R : Type ?u.705600
S : Type u_2
T : Type ?u.705606
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_1
B : Type ?u.705912
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type ?u.706334
inst✝⁴ : Field K
S' : Type u_3
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
⊢ equivOfRoot pb (map pb e) h₁ h₂ = e
ext x
case h.intro
R : Type ?u.705600
S : Type u_2
T : Type ?u.705606
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_1
B : Type ?u.705912
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type ?u.706334
inst✝⁴ : Field K
S' : Type u_3
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ↑(equivOfRoot pb (map pb e) h₁ h₂) (↑(aeval pb.gen) f) = ↑e (↑(aeval pb.gen) f)
case h
R : Type ?u.705600
S : Type u_2
T : Type ?u.705606
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_1
B : Type ?u.705912
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type ?u.706334
inst✝⁴ : Field K
S' : Type u_3
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
x : S
⊢ ↑(equivOfRoot pb (map pb e) h₁ h₂) x = ↑e x
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
no goals
case h.intro
R : Type ?u.705600
S : Type u_2
T : Type ?u.705606
inst✝¹¹ : CommRing R
inst✝¹⁰ : Ring S
inst✝⁹ : Algebra R S
A : Type u_1
B : Type ?u.705912
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Algebra A B
K : Type ?u.706334
inst✝⁴ : Field K
S' : Type u_3
inst✝³ : CommRing S'
inst✝² : Algebra R S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : ↑(aeval pb.gen) (minpoly A (map pb e).gen) = 0
h₂ : ↑(aeval (map pb e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ↑(equivOfRoot pb (map pb e) h₁ h₂) (↑(aeval pb.gen) f) = ↑e (↑(aeval pb.gen) f)
simp [aeval_algEquiv]