A : Type u_2
B : Type u_1
B' : Type ?u.21842
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False
A : Type u_2
B : Type u_1
B' : Type ?u.21842
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
⊢ minpoly A x ≠ 1
intro h
A : Type u_2
B : Type u_1
B' : Type ?u.21842
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0
A : Type u_2
B : Type u_1
B' : Type ?u.21842
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False
refine' (one_ne_zero : (1 : B) ≠ 0) _
no goals
A : Type u_2
B : Type u_1
B' : Type ?u.21842
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0
simpa using congr_arg (Polynomial.aeval x) h