R : Type ?u.135537
S : Type u_2
T : Type ?u.135543
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.135849
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.136271
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ minpolyGen pb = minpoly A pb.gen
R : Type ?u.135537
S : Type u_2
T : Type ?u.135543
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.135849
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.136271
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ minpolyGen pb = minpoly A pb.gen
nontriviality A
R : Type ?u.135537
S : Type u_2
T : Type ?u.135543
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.135849
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.136271
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
q : A[X]
hq : degree q < degree (minpolyGen pb)
hn0 : ¬q = 0
h0 : ↑(aeval pb.gen) q = 0
⊢ False
R : Type ?u.135537
S : Type u_2
T : Type ?u.135543
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.135849
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.136271
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
⊢ minpolyGen pb = minpoly A pb.gen
refine' minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
  or_iff_not_imp_left.2 fun hn0 h0 => _
no goals
R : Type ?u.135537
S : Type u_2
T : Type ?u.135543
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Algebra R S
A : Type u_1
B : Type ?u.135849
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : Algebra A B
K : Type ?u.136271
inst✝¹ : Field K
inst✝ : Algebra A S
pb : PowerBasis A S
✝ : Nontrivial A
q : A[X]
hq : degree q < degree (minpolyGen pb)
hn0 : ¬q = 0
h0 : ↑(aeval pb.gen) q = 0
⊢ False
exact (pb.dim_le_degree_of_root hn0 h0).not_lt (pb.degree_minpolyGen ▸ hq)