Theorem: Polynomial.Separable.scaleRoots (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : p.Separable
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).Separable
Tactic:
delta Polynomial.Separable at hp ⊢
State after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) (derivative (p.scaleRoots r))

State before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) (derivative (p.scaleRoots r))
Tactic:
rw [Polynomial.derivative_scaleRoots, Algebra.smul_def]
State after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r)
    ((algebraMap R R[X]) (r ^ (p.natDegree - ((derivative p).natDegree + 1))) * (derivative p).scaleRoots r)

State before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r)
    ((algebraMap R R[X]) (r ^ (p.natDegree - ((derivative p).natDegree + 1))) * (derivative p).scaleRoots r)
Tactic:
refine (isCoprime_mul_unit_left_right ((hr.pow _).map _) _ _).mpr ?_
State after:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) ((derivative p).scaleRoots r)

State before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : IsCoprime p (derivative p)
r : R
hr : IsUnit r
⊢ IsCoprime (p.scaleRoots r) ((derivative p).scaleRoots r)
Tactic:
exact Polynomial.isCoprime_scaleRoots _ _ _ hr hp
State after:
no goals