no goals
R : Type u
S✝ : Type v
K : Type w
inst✝⁴ : CommRing R
f✝ : R[X]
inst✝³ : CommRing S✝
i : R →+* S✝
a : S✝
h : eval₂ i a f✝ = 0
inst✝² : Algebra R S✝
hfx : ↑(aeval a) f✝ = 0
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (↑C r * X - 1) →ₐ[R] S
⊢ ↑(algebraMap R S) r * ↑f (root (↑C r * X - 1)) = 1
rw [← f.commutes, ← f.map_mul, algebraMap_eq, root_isInv, map_one]
no goals
R : Type u
S✝ : Type v
K : Type w
inst✝⁴ : CommRing R
f✝ : R[X]
inst✝³ : CommRing S✝
i : R →+* S✝
a : S✝
h : eval₂ i a f✝ = 0
inst✝² : Algebra R S✝
hfx : ↑(aeval a) f✝ = 0
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (↑C r * X - 1) →ₐ[R] S
⊢ ↑(algebraMap R S) r * ↑g (root (↑C r * X - 1)) = 1
rw [← g.commutes, ← g.map_mul, algebraMap_eq, root_isInv, map_one]