case pos
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

case neg
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
⊢ map f (minpoly A x) ≠ 1
by_cases hx : IsIntegral A x
no goals
case pos
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)
case neg
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ 0 ≠ 1
case neg
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
rw [eq_zero hx, Polynomial.map_zero]
no goals
case neg
A : Type u_3
B : Type u_1
B' : Type ?u.27580
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ 0 ≠ 1
exact zero_ne_one