A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
case hp1
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Irreducible (p * ↑C (leadingCoeff p)⁻¹)

case hp2
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0

case hp3
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Monic (p * ↑C (leadingCoeff p)⁻¹)
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ p * ↑C (leadingCoeff p)⁻¹ = minpoly A x
apply eq_of_irreducible_of_monic
no goals
case hp1
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Irreducible (p * ↑C (leadingCoeff p)⁻¹)
exact Associated.irreducible ⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff,
  by rwa [← C_mul, inv_mul_cancel, C_1], by rwa [← C_mul, mul_inv_cancel, C_1]⟩, rfl⟩ hp1
no goals
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑C (leadingCoeff p)⁻¹ * ↑C (leadingCoeff p) = 1
rwa [← C_mul, inv_mul_cancel, C_1]
no goals
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑C (leadingCoeff p) * ↑C (leadingCoeff p)⁻¹ = 1
rwa [← C_mul, mul_inv_cancel, C_1]
no goals
case hp2
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ ↑(Polynomial.aeval x) (p * ↑C (leadingCoeff p)⁻¹) = 0
rw [aeval_mul, hp2, MulZeroClass.zero_mul]
no goals
case hp3
A : Type u_2
B : Type u_1
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : ↑(Polynomial.aeval x) p = 0
this : leadingCoeff p ≠ 0
⊢ Monic (p * ↑C (leadingCoeff p)⁻¹)
rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel]