R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ (↑x)⁻¹ ∈ A
suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
  rw [this]
  exact A.smul_mem (aeval x _).2 _
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
have : aeval (x : L) p = 0 := by rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ -((↑(algebraMap K L) (coeff p 0))⁻¹ * ↑(aeval ↑x) (divX p)) =
    ↑(↑(algebraMap K ((fun x => { x // x ∈ A }) (divX p))) (-coeff p 0)⁻¹ * ↑(aeval x) (divX p))
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
rw [inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne, div_eq_inv_mul, Algebra.smul_def]
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ -((↑(algebraMap K L) (coeff p 0))⁻¹ * ↑(↑(aeval x) (divX p))) =
    ↑(algebraMap K L) (-coeff p 0)⁻¹ * ↑(↑(aeval x) (divX p))
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ -((↑(algebraMap K L) (coeff p 0))⁻¹ * ↑(aeval ↑x) (divX p)) =
    ↑(↑(algebraMap K ((fun x => { x // x ∈ A }) (divX p))) (-coeff p 0)⁻¹ * ↑(aeval x) (divX p))
simp only [aeval_coe, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, coe_toSubsemiring,
  coe_algebraMap]
no goals
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : ↑(aeval ↑x) p = 0
⊢ -((↑(algebraMap K L) (coeff p 0))⁻¹ * ↑(↑(aeval x) (divX p))) =
    ↑(algebraMap K L) (-coeff p 0)⁻¹ * ↑(↑(aeval x) (divX p))
rw [map_inv₀, map_neg, inv_neg, neg_mul]
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
⊢ ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p)) ∈ A
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
⊢ (↑x)⁻¹ ∈ A
rw [this]
no goals
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
this : (↑x)⁻¹ = ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p))
⊢ ↑((-coeff p 0)⁻¹ • ↑(aeval x) (divX p)) ∈ A
exact A.smul_mem (aeval x _).2 _
no goals
R : Type ?u.788449
S : Type ?u.788452
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing S
K : Type u_2
L : Type u_1
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : { x // x ∈ A }
p : K[X]
aeval_eq : ↑(aeval x) p = 0
coeff_zero_ne : coeff p 0 ≠ 0
⊢ ↑(aeval ↑x) p = 0
rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]