mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ (∑ s, X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k =
    ∑ s, (X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ f = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
r : R
f : R →+* S
⊢ map f ((taylor r) p) = (taylor (f r)) (map f p)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
r s : R
⊢ (taylor r) ((taylor s) f) = (taylor (r + s)) f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
f : R[X]
s : R
⊢ eval s ((taylor r) f) = eval (s + r) f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y t : R
⊢ ((taylor x) p).natDegree < ((taylor x) p).natDegree + 2

Tactic:
by

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ (∑ i ∈ Finset.range p.natDegree, ((taylor x) p).coeff (i + 2) * y ^ i) * y ^ 2 + eval x (derivative p) * y +
      eval x p =
    ∑ k ∈ Finset.range ((taylor x) p).natDegree, ((taylor x) p).coeff (k + 1 + 1) * y ^ (k + 1 + 1) +
        ((taylor x) p).coeff (0 + 1) * y ^ (0 + 1) +
      ((taylor x) p).coeff 0 * y ^ 0

Tactic:
simp [pow_succ, mul_assoc, Finset.sum_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
⊢ ∃ c, c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ {s | #s = k} = powersetCard k univ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
hy : y ^ 2 = 0
⊢ eval (x + y) p = eval x p + eval x (derivative p) * y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R[X]
x y : S
hy : y ^ 2 = 0
⊢ (aeval (x + y)) p = (aeval x) p + (aeval x) (derivative p) * y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r✝ : R
f : R[X]
r : R
P : R[X]
⊢ (taylorAlgHom (-r)) ((↑↑(taylorAlgHom r).toRingHom).toFun P) = P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r✝ : R
f : R[X]
r : R
P : R[X]
⊢ (↑↑(taylorAlgHom r).toRingHom).toFun ((taylorAlgHom (-r)) P) = P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
f : R[X]
s : R
⊢ eval (s - r) ((taylor r) f) = eval s f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ ∑ s, (X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ (((taylor r) f).sum fun i a ↦ C a * (X - C r) ^ i) = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
⊢ (1 + X • M.map ⇑C).det.coeff k = ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
i : ℕ
⊢ (p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : R
⊢ scaleRoots 0 s = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
⊢ p.scaleRoots s ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).support ⊆ p.support

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
⊢ p.support ⊆ (p.scaleRoots s).support

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
⊢ M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).natDegree = p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ (p.scaleRoots r).leadingCoeff = p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).Monic ↔ p.Monic

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : f p.leadingCoeff ≠ 0
⊢ map f (p.scaleRoots x) = (map f p).scaleRoots (f x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r c : R
⊢ (C c).scaleRoots r = C c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 1 = p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ M.charpolyRev = (1 + X • (-M).map ⇑C).det

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ scaleRoots 1 r = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
s : Finset n
hs : s ∈ powersetCard k univ
⊢ (-1) ^ #s * (M.submatrix Subtype.val Subtype.val).det = (-1) ^ k * (M.submatrix Subtype.val Subtype.val).det

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
⊢ M.charpoly.coeff (Fintype.card n - k) =
    (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r s : R
⊢ (X + C r).scaleRoots s = X + C (r * s)

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ eval₂ f (f s * a) (p.scaleRoots s) =
    ∑ i ∈ (p.scaleRoots s).support, f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
⊢ p.coeff i * s ^ (p.natDegree - i) = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i = f s ^ p.natDegree * (f (p.coeff i) * a ^ i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ ∑ i ∈ p.support, f s ^ p.natDegree * (f (p.coeff i) * a ^ i) = f s ^ p.natDegree * eval₂ f a p

Tactic:
by

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * eval₂ f a p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring S
inst✝ : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ eval₂ f (f s * r) (p.scaleRoots s) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ (aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ integralNormalization 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
hx : x ≠ 0
⊢ (C x).integralNormalization = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.support ⊆ p.support

Tactic:
by

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

Goal state before:
pp: S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
⊢ eval₂ f (f r) (p.scaleRoots s) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : p.degree = ↑i
⊢ p.integralNormalization.coeff i = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r s : R
⊢ p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : p.degree ≠ ↑i
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.coeff p.natDegree ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.degree = p.degree

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization * C p.leadingCoeff = p.scaleRoots p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: S : Type v
inst✝ : CommSemiring S
p : S[X]
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n = 0 → p.leadingCoeff ^ (n + 1) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
hp : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
by

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
hn : (p + q).natDegree < n
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
⊢ r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
f : R →+* A
p : R[X]
H : f p.leadingCoeff ≠ 0
⊢ (map f p).integralNormalization = map f p.integralNormalization

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
s : R := ↑hr.unit⁻¹
⊢ (a * p).natDegree = (b * q).natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
⊢ f.integralNormalization.support = f.support

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
h : IsCoprime p q
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
s : S
p : MvPolynomial σ N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgEquiv (s ⊗ₜ[R] p)) = s ⊗ₜ[R] coeff d p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
e : σ →₀ ℕ
s : S
n : N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgEquiv (s ⊗ₜ[R] (monomial e) n)) = if e = d then s ⊗ₜ[R] n else 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (AlgHom.restrictScalars R ↑(algebraTensorAlgEquiv R A).symm).comp (mapAlgHom (Algebra.ofId R A)) =
    Algebra.TensorProduct.includeRight

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i : σ
⊢ (tensorEquivSum R σ ι S) (X i ⊗ₜ[R] 1) = X (Sum.inl i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : S
⊢ (tensorEquivSum R σ ι S) (C r ⊗ₜ[R] 1) = C r

Tactic:
by

Goal state after: