K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x → IsIntegral K x
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x ↔ IsIntegral K x
refine' ⟨_, IsIntegral.isAlgebraic K⟩
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : ↑(aeval x) p = 0
⊢ IsIntegral K x
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x → IsIntegral K x
rintro ⟨p, hp, hpx⟩
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap K A) x (p * ↑C (leadingCoeff p)⁻¹) = 0
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : ↑(aeval x) p = 0
⊢ IsIntegral K x
refine' ⟨_, monic_mul_leadingCoeff_inv hp, _⟩
no goals
case intro.intro
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap K A) x (p * ↑C (leadingCoeff p)⁻¹) = 0
rw [← aeval_def, AlgHom.map_mul, hpx, MulZeroClass.zero_mul]