A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
⊢ minpoly A x = 1
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
⊢ minpoly A x = 1
nontriviality A
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ degree 1
⊢ minpoly A x = 1
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
⊢ minpoly A x = 1
have := minpoly.min A x monic_one (Subsingleton.elim _ _)
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ degree 1
⊢ minpoly A x = 1
rw [degree_one] at this
case inl
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1

case inr
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : 0 < degree (minpoly A x)
⊢ minpoly A x = 1
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
cases' le_or_lt (minpoly A x).degree 0 with h h
no goals
case inl
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
rwa [(monic ⟨1, monic_one, by simp⟩ : (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h
no goals
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ eval₂ (algebraMap A B) x 1 = 0
simp
no goals
case inr
A : Type u_2
B : Type u_1
B' : Type ?u.53832
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : 0 < degree (minpoly A x)
⊢ minpoly A x = 1
exact (this.not_lt h).elim