R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) p = ↑(aeval x) (divX p) * x + ↑(algebraMap K L) (coeff p 0)

R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ x⁻¹ = ↑(aeval x) (divX p) / (↑(aeval x) p - ↑(algebraMap K L) (coeff p 0))
rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]
R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p * X + ↑C (coeff p 0)) = ↑(aeval x) (divX p) * x + ↑(algebraMap K L) (coeff p 0)

R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) p = ↑(aeval x) (divX p) * x + ↑(algebraMap K L) (coeff p 0)

R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
conv_lhs => rw [← divX_mul_X_add p]
R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p * X + ↑C (coeff p 0)) = ↑(aeval x) (divX p) * x + ↑(algebraMap K L) (coeff p 0)

R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
rw [AlgHom.map_add, AlgHom.map_mul, aeval_X, aeval_C]
no goals
R : Type ?u.584800
S : Type ?u.584803
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : L
p : K[X]
aeval_ne : ↑(aeval x) (divX p) ≠ 0
⊢ ↑(aeval x) (divX p) ≠ 0
exact aeval_ne