A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ p = minpoly A x
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
⊢ p = minpoly A x
have hx : IsIntegral A x := ⟨p, pmonic, hp⟩
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x = p
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ p = minpoly A x
symm
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x - p = 0
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x = p
apply eq_of_sub_eq_zero
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ False
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
⊢ minpoly A x - p = 0
by_contra hnz
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : degree (minpoly A x) ≤ degree (minpoly A x - p)
⊢ False
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ False
have hd := degree_le_of_ne_zero A x hnz (by simp [hp])
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x - p) < degree (minpoly A x)
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : degree (minpoly A x) ≤ degree (minpoly A x - p)
⊢ False
contrapose! hd
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ leadingCoeff (minpoly A x) = leadingCoeff p

A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x) = degree p
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x - p) < degree (minpoly A x)
apply degree_sub_lt _ (minpoly.ne_zero hx)
no goals
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
⊢ ↑(Polynomial.aeval x) (minpoly A x - p) = 0
simp [hp]
no goals
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ leadingCoeff (minpoly A x) = leadingCoeff p
rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]
no goals
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), Monic q → ↑(Polynomial.aeval x) q = 0 → degree p ≤ degree q
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
hd : ¬False
⊢ degree (minpoly A x) = degree p
exact le_antisymm (min A x pmonic hp) (pmin (minpoly A x) (monic hx) (aeval A x))