mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ r.natDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p * C q.leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
⊢ rootMultiplicity x (X - C y) = if x = y then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ ↑q.natDegree ≤ ↑p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.degree = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
⊢ map f ((expand R p) q) = (expand S p) (map f q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r a : R
⊢ eval r ((expand R p) (C a)) = eval (r ^ p) (C a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
⊢ (p %ₘ q).degree < q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
n : ℕ
a : R
x✝ : eval r ((expand R p) (C a * X ^ n)) = eval (r ^ p) (C a * X ^ n)
⊢ eval r ((expand R p) (C a * X ^ (n + 1))) = eval (r ^ p) (C a * X ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree → (p %ₘ q).degree < q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
⊢ eval r ((expand R p) P) = eval (r ^ p) P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ (aeval r) ((expand R p) (C a)) = (aeval (r ^ p)) (C a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
x✝ : (aeval r) ((expand R p) (C a * X ^ n)) = (aeval (r ^ p)) (C a * X ^ n)
⊢ (aeval r) ((expand R p) (C a * X ^ (n + 1))) = (aeval (r ^ p)) (C a * X ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).Monic

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬p ≠ 0 → (p %ₘ q).degree < q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : Associated p q
⊢ p.degree = q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ (aeval r) ((expand R p) P) = (aeval (r ^ p)) P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 %ₘ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 /ₘ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p %ₘ 0 = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree + 1 ≤ n * 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Prime X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ n * 1 ≤ n * p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial (n + 1)) a) = (monomial n) (a * (↑n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ (contract p f).coeff n = f.coeff (n * p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p %ₘ 0 = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X) = C a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
hp : p ≠ 0
f : R →+* S
q : R[X]
n : ℕ
⊢ (map f (contract p q)).coeff n = (contract p (map f q)).coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p /ₘ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ p = X - C (-p.coeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
⊢ contract p ((expand R p) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ (contract 1 f).coeff n = f.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
r : R
⊢ contract p (C r) = C r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p /ₘ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative (C a * X ^ n) = C (a * ↑n) * X ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h : IsUnit p
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f + g) = contract p f + contract p g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X ^ 2) = C (a * 2) * X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (X ^ n) = C ↑n * X ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (X ^ (n + 1)) = C (↑n + 1) * X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ derivative (X ^ 2) = C 2 * X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ derivative p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ X ∣ p - C (p.coeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (monomial (1 - 1)) (1 * ↑1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ derivative (X + C c) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ (⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
this : DecidableEq R := Classical.decEq R
H : p = 0
⊢ (derivative p).degree = p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 * p, (x, y).2 * p) = (p * x, p * y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
⊢ IsUnit f ∨ IsUnit g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f * (expand R p) g) = contract p f * g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ Irreducible (C a * X + C b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ((⇑derivative)^[k] p).natDegree ≤ p.natDegree - k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p a * f + contract p b * g = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
⊢ (aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative ↑n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ -C ↑h.unit⁻¹ * (X - C a) + C ↑h.unit⁻¹ * (X - C b) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ q ∣ p %ₘ q - p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ q ∣ p %ₘ q ↔ q ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
⊢ p.degree < q.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
⊢ (expand R p) (contract p f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
⊢ (X - C x).degree ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
⊢ (expand R p) (contract p f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p /ₘ q = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ↑(x ::ₘ t).card = ↑t.card + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ p /ₘ q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree ≤ (q * (p /ₘ q)).degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ↑t.card + 1 ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
⊢ (⇑derivative)^[x] p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ map (frobenius R p) ((expand R p) f) = f ^ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
⊢ map (iterateFrobenius R p n) ((expand R (p ^ n)) f) = f ^ p ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f g : R[X]
⊢ derivative (f * g) = derivative f * g + f * derivative g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (derivative p) = p.sum fun n a ↦ a * ↑n * x ^ (n - 1)

Tactic:
by

Goal state after: