A : Type u_1
B : Type u_2
B' : Type ?u.2178
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (if hx : IsIntegral A x then
      WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)
A : Type u_1
B : Type u_2
B' : Type ?u.2178
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic (minpoly A x)
delta minpoly
A : Type u_1
B : Type u_2
B' : Type ?u.2178
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx)
A : Type u_1
B : Type u_2
B' : Type ?u.2178
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (if hx : IsIntegral A x then
      WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)
rw [dif_pos hx]
no goals
A : Type u_1
B : Type u_2
B' : Type ?u.2178
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx)
exact (degree_lt_wf.min_mem _ hx).1