A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
⊢ x ∈ RingHom.range (algebraMap A B)
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
⊢ x ∈ RingHom.range (algebraMap A B)
have h : IsIntegral A x := by
  by_contra h
  rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
  exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ RingHom.range (algebraMap A B)
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
⊢ x ∈ RingHom.range (algebraMap A B)
have key := minpoly.aeval A x
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : x = ↑(algebraMap A B) (-coeff (minpoly A x) 0)
⊢ x ∈ RingHom.range (algebraMap A B)
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ RingHom.range (algebraMap A B)
rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add,
  aeval_C, aeval_X, ← eq_neg_iff_add_eq_zero, ← RingHom.map_neg] at key
no goals
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : x = ↑(algebraMap A B) (-coeff (minpoly A x) 0)
⊢ x ∈ RingHom.range (algebraMap A B)
exact ⟨-(minpoly A x).coeff 0, key.symm⟩
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
⊢ IsIntegral A x
by_contra h
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
⊢ False
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
no goals
A : Type u_1
B : Type u_2
B' : Type ?u.31272
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False
exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx