mathlib-initiative/mathlib-tactics huggingface dataset:
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) (1 ⊗ₜ[R] X i) = X (Sum.inr 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 : R
⊢ (tensorEquivSum R σ ι S) (1 ⊗ₜ[R] C r) = C ((algebraMap R S) r)

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 : R
s : S
⊢ (tensorEquivSum R σ ι S) (C s ⊗ₜ[R] C r) = C (r • s)

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 : σ
j : ι
⊢ (tensorEquivSum R σ ι S) (X i ⊗ₜ[R] X j) = X (Sum.inl i) * X (Sum.inr j)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ Splits 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ X.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ X.Splits

Tactic:
by
  simpa using Splits.X_add_C (0 : R)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((Polynomial.monomial n) a).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
⊢ q ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i f).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ ↑((p.toSubring T hp).coeff n) = p.coeff n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
H : (p.toSubring T hp).coeff i = 0
⊢ ↑0 = 0

Tactic:
ZeroMemClass.coe_zero

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
H : (p.toSubring T hp).coeff i = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
H : (p.toSubring T hp).coeff i = 0
⊢ ↑((p.toSubring T hp).coeff i) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).support = p.support

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).degree = p.degree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).natDegree = p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
h : Invertible (C a * X + C b).leadingCoeff
ha : a ≠ 0
⊢ Invertible a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
H : (p.toSubring T hp).coeff p.natDegree = 1
⊢ ↑((p.toSubring T hp).coeff p.natDegree) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).Monic ↔ p.Monic

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ ↑(coeffs 0) ⊆ ↑T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
⊢ toSubring 0 T ⋯ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 1 T ⋯).coeff i) = ↑(coeff 1 i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ map T.subtype (p.toSubring T hp) = p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = ↑0

Tactic:
ZeroMemClass.coe_zero

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ (ofSubring T p).coeff n = ↑(p.coeff n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree ≤ 1
h : Invertible f.leadingCoeff
⊢ f.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
⊢ ↑(ofSubring T p).coeffs ⊆ ↑T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r i : R
⊢ (X + C r + C i).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
⊢ ((Polynomial.taylor r) p).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
⊢ mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).roots = Multiset.map (fun x ↦ r * x) p.roots

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∀ f ∈ Multiset.map (fun x ↦ X + C x) m, f.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ f.Splits ↔ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
⊢ m = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
⊢ f.natDegree ≤ 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : AddCommMonoid M
a : A
m : M
b : B
⊢ AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun (AddMonoidAlgebra.single m (a ⊗ₜ[R] b)) =
    a ⊗ₜ[R] AddMonoidAlgebra.single m b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : CommMonoid M
a : A
m : M
b : B
⊢ invFun (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
a : R
⊢ ((X + C a).comp g).natDegree ≤ 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
⊢ (f.comp g).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
e : A →ₐ[R] B
⊢ (map (algebraMap R B) f).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a : R
⊢ (X - C a).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
⊢ A ⊗[R] B[M] ≃ₐ[S] (A ⊗[R] B)[M]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (-f).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (comp 1 (-X)).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : CommMonoid M
a : A
p : B[M]
⊢ (rTensorEquivAlgEquiv R S A B) (a ⊗ₜ[R] p) = a • (mapAlgHom M includeRight) p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
B : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : CommSemiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : CommMonoid M
m : M
a : A
b : B
⊢ (lTensorAlgEquiv R A B).symm (single m (a ⊗ₜ[R] b)) = single m a ⊗ₜ[R] b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
a : A
p : R[M]
⊢ (scalarTensorEquiv R A) (a ⊗ₜ[R] p) = a • (mapAlgHom M (ofId R A)) p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
m : M
a : A
⊢ (scalarTensorEquiv R A).symm (single m a) = a ⊗ₜ[R] single m 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (f.comp (-X)).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
x : A[M]
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] x) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
m : M
r₁ : R
n : N
r₂ : R
⊢ (tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂) = single (m, n) (r₁ * r₂)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
mn : M × N
r : R
⊢ (tensorEquiv R).symm (single mn r) = single mn.1 1 ⊗ₜ[R] single mn.2 r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
mn : M × N
r : R
⊢ (tensorEquiv R).symm (single mn r) = single mn.1 r ⊗ₜ[R] single mn.2 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (Multiset.map (fun x ↦ -x) m)).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) (Multiset.map (fun x ↦ -x) m)).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ f.Splits ↔ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (a ::ₘ m)).prod
ha : a ∈ a ::ₘ m
⊢ eval a f = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
⊢ ∃ a, eval a f = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf✝ : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
hf : f.roots = m
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
⊢ f = (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
x : R
⊢ eval x f = f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) f.roots).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
x : R
⊢ eval x f = (Multiset.map (fun x_1 ↦ x - x_1) f.roots).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
f : R[X]
A : Type u_2
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : Algebra R A
hf : (map (algebraMap R A) f).Splits
hm : f.Monic
x : A
⊢ (aeval x) f = (Multiset.map (fun x_1 ↦ x - x_1) (f.aroots A)).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hf : f.Splits
x : R
⊢ eval x (derivative f) =
    f.leadingCoeff * (Multiset.map (fun a ↦ (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase a)).prod) f.roots).sum

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hf : f.Splits
hm : f.Monic
x : R
hx : x ∈ f.roots
⊢ eval x (derivative f) = (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase x)).prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi✝ : Function.Injective ⇑i
hf : (map i f).Splits
hi : ∀ a ∈ (map i f).roots, a ∈ i.range
⊢ f.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
⊢ f ∈ lifts i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
x : R
hr : f.roots = {x}
⊢ f = C f.leadingCoeff * (X - C x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
⊢ f.natDegree = f.roots.card

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : f.natDegree ≠ 0
⊢ f.roots ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
φ : R →+* S
hφ : map φ f ≠ 0
⊢ (map φ f).roots = Multiset.map (⇑φ) f.roots

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
φ : A →ₐ[R] B
hφ : map (algebraMap R B) f ≠ 0
⊢ map (↑φ) (map (algebraMap R A) f) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
⊢ ∃ b, x * b = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
⊢ x⁻¹ ∈ R[x]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
A : Subalgebra R S
int : IsIntegral R x
inv_mem : x⁻¹ ∈ A
⊢ x ∈ A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : IsDomain A
inst✝² : IsDomain B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
φ : A →ₐ[R] B
hφ : map (algebraMap R B) f ≠ 0
⊢ ⇑φ '' f.rootSet A = f.rootSet B

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
h' : FiniteType R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ⊤.FG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
hx : IsIntegral R x
⊢ R[x] ≤ integralClosure R A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
⊢ f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
⊢ f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
⊢ f.nextCoeff = -f.leadingCoeff * f.roots.sum

Tactic:
by

Goal state after: