R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ coeff (normalizeScaleRoots p) (natDegree (normalizeScaleRoots p)) = 1
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ Monic (normalizeScaleRoots p)
delta Monic leadingCoeff
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ coeff (normalizeScaleRoots p) (natDegree p) = 1
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ coeff (normalizeScaleRoots p) (natDegree (normalizeScaleRoots p)) = 1
rw [natDegree_eq_of_degree_eq (normalizeScaleRoots_degree p)]
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ p = 0 → 0 = 1
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ coeff (normalizeScaleRoots p) (natDegree p) = 1
suffices p = 0 → (0 : R) = 1 by simpa [normalizeScaleRoots, coeff_monomial]
no goals
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
⊢ p = 0 → 0 = 1
exact fun h' => (h h').elim
no goals
R : Type u_1
A : Type ?u.937581
B : Type ?u.937584
S : Type ?u.937587
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
p : R[X]
x : S
h : p ≠ 0
this : p = 0 → 0 = 1
⊢ coeff (normalizeScaleRoots p) (natDegree p) = 1
simpa [normalizeScaleRoots, coeff_monomial]