mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
k : ℕ
⊢ (X ^ k).content = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ X.content = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
⊢ (C r * p).content = normalize r * p.content

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
this : map (algebraMap T S) p * map (algebraMap T S) q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
⊢ Associated (C r * p).content (r * p.content)

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
r : T
⊢ (X - C r).aroots S = {(algebraMap T S) r}

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ X.aroots S = {0}

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).aroots S = 0

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ aroots 0 S = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ ((monomial k) r).content = normalize r

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
⊢ (-p).aroots S = p.aroots S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = 0 ↔ p = 0

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (C a * p).aroots S = p.aroots S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ normUnit p.content = 1

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (a • p).aroots S = p.aroots S

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ (p ^ n).aroots S = n • p.aroots S

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
n : ℕ
⊢ (X ^ n).aroots S = n • {0}

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ (C a * X ^ n).aroots S = n • {0}

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).aroots S = n • {0}

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map (algebraMap T S) p).aroots R = p.aroots R

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ p.rootSet S = ↑(p.aroots S).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ p.content = (Finset.range n).gcd p.coeff

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ WellFounded DvdNotUnit

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).rootSet S = ∅

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ rootSet 0 S = ∅

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ rootSet 1 S = ∅

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ (-p).rootSet S = p.rootSet S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
⊢ Set.Finite fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
⊢ Irreducible p ↔ Prime p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
h : e.symm a = 0
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝⁵ : CommRing T
p : T[X]
S : Type u_1
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : S
⊢ a ∈ p.rootSet S ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
⊢ (fun x ↦ eval x p) ⁻¹' {a} = (p - C a).rootSet R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ (Multiset.map (⇑e) w).prod * ↑((Units.map e.toMonoidHom) u) = a

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
hp : p.Monic
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ (aeval a) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
⊢ UniqueFactorizationMonoid β

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ C r ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
⊢ a ∣ b * c → a ∣ c

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬(X - C t) ^ m ∣ derivative p

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : x ∈ p.rootSet S
⊢ f x ∈ p.rootSet S'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ p.content = 1

Tactic:
by

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ p.rootSet S
hf : p = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S') p = map (algebraMap T S') 0

Tactic:
by

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

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = C p.content * p.primPart

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
p : S[X]
inst✝ : Algebra S R
h : Function.Injective ⇑(algebraMap S R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ (aeval x) p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h✝ : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
h : derivative p = 0
⊢ (X - C t) ^ m ∣ derivative p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
a : R
⊢ ↑(nthRootsFinset n a) = {r | r ^ n = a}

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
g : G
x : R
hx : x ∈ f.rootSet R
⊢ g • x ∈ f.rootSet R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.IsPrimitive

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
hnezero : derivative p ≠ 0
⊢ rootMultiplicity t (derivative p) ≤ m - 1

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
⊢ g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.natDegree = p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ p.primPart = p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ C ↑(normUnit r)⁻¹ * C ↑(normUnit r) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ Fintype.card ↑(Set.range f) = #(image f univ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ C ↑(normUnit r) * C ↑(normUnit r)⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ IsUnit (C r).primPart

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
⊢ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : NormalizedGCDMonoid R
S : Type u_2
inst✝³ : Ring S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Module.IsTorsionFree R S
p : R[X]
s : S
hpzero : p ≠ 0
hp : (aeval s) p = 0
⊢ (aeval s) p.primPart = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
⊢ ∀ (a : R), a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s p = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
⊢ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
⊢ Fintype { x // x ∣ y }

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : f ≠ 0
hfR : ↑f.natDegree < #R
⊢ ∃ r, eval r f ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
inst✝ : DecidableEq R
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod = ∏ a ∈ p.roots.toFinset, (X - C a) ^ rootMultiplicity a p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a p.content = gcd a q.content

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ eval t ((⇑derivative)^[rootMultiplicity t p] p) =
    (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n ! ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
⊢ ↑(rootMultiplicity t p)! ∣ ↑n !

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ count r s ≤ count r p.roots

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
⊢ (Multiset.map (fun a ↦ X - C a) s).prod ∣ p ↔ s ≤ p.roots

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ↑n ! ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (↑a + ↑b).prod = FactorSet.prod ↑a * FactorSet.prod ↑b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
⊢ ⊤.prod ≤ b.prod

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ ↑1! ∈ nonZeroDivisors R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h✝ : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
⊢ 0 ≤ 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h✝ : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
⊢ 1 ≤ 1

Tactic:
by

Goal state after: