mathlib-initiative/mathlib-tactics huggingface dataset:
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.nextCoeff = -f.roots.sum

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
ι : Sort u_5
S : ι → Subalgebra R A
⊢ Algebra.IsIntegral R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral R ↥(S i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
⊢ Subalgebra.map (↑f) (integralClosure R A) = integralClosure R S

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 : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x) p = 0
⊢ ↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
hx : IsIntegral R (x * y)
⊢ IsIntegral R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
h : IsIntegral R x
n : ℕ
⊢ x ∈ R[x]

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
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R M.det

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
h'' : p = 0
⊢ False

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
a : R
⊢ ((X - C a) * f).Splits ↔ f.Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
⊢ i ∈ p.support

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
⊢ n + 1 ≠ Zero.zero

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
⊢ Function.Injective ⇑(mapRingHom (algebraMap R S))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
this : Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
⊢ integerNormalization M p = 0 ↔ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
⊢ ∃ b, Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p

Tactic:
by

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

Goal state before:
pp: case succ.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
this : X - C a ∣ f ∨ X - C a ∣ g
hf2 :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (n : ℕ)
    (ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits)
    {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n + 1)
    (a : R) (ha : eval a p = 0) (this : X - C a ∣ f ∨ X - C a ∣ g), X - C a ∣ f → f.Splits ∧ g.Splits
hf : ¬X - C a ∣ f
⊢ f.Splits ∧ g.Splits

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
this : X - C a ∣ f ∨ X - C a ∣ g
hf : X - C a ∣ f
⊢ f.Splits ∧ g.Splits

Tactic:
· exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
this : X - C a ∣ f ∨ X - C a ∣ g
hf : X - C a ∣ f
⊢ f.Splits ∧ g.Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
R' : Type u_3
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ (aeval x) (integerNormalization M p) = 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
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ X - C a ≠ 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
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ f * g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : (aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
⊢ (Polynomial.map (algebraMap A K) p).coeff i = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x ↔ IsAlgebraic K x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
⊢ f ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : (aeval x) p = 0
⊢ IsIntegral R (p.leadingCoeff • x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
⊢ (f * g).Splits ↔ f.Splits ∧ g.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hpq : (f * g).Splits
⊢ (f.Splits ∨ g = 0) ∧ (g.Splits ∨ f = 0)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
⊢ (f.Splits ∨ g = 0) ∧ (g.Splits ∨ f = 0) → (f * g).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hg₀ : g ≠ 0
hg : g.Splits
⊢ (f * g).Splits ↔ f.Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg : f.Splits
⊢ (f * g).Splits ↔ g.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
⊢ (X * f).Splits ↔ 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
⊢ (f * X).Splits ↔ 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
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ 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
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ g ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hg : g.Splits
hg₀ : g ≠ 0
hfg : f ∣ g
⊢ f.Splits

Tactic:
by

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ eval₂ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) ((Ideal.Quotient.mk I) X) g = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem ((Ideal.Quotient.mk I) X)

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 : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
by

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'

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 : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
⊢ (IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)

Tactic:
by

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ S[(Ideal.Quotient.mkₐ S I) X] = ⊤

Tactic:
by

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral

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
⊢ (∃ y, (algebraMap (↥(integralClosure R A)) A) y = x) → IsIntegral R x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Module R A
inst✝¹ : IsScalarTower R A B
inst✝ : IsTorsionFree R B
⊢ IsTorsionFree R A

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 1
⊢ (algebraMap A B) (mk' A 1 h) = (algebraMap A B) 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : IsIntegral R 0
⊢ (algebraMap A B) (mk' A 0 h) = (algebraMap A B) 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ (algebraMap A B) (mk' A (x + y) ⋯) = (algebraMap A B) (mk' A x hx + mk' A y hy)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : (map i f).IsRoot x
⊢ x ∈ i.range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ (algebraMap A B) (mk' A (x * y) ⋯) = (algebraMap A B) (mk' A x hx * mk' A y hy)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsIntegralClosure A R B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
x : R
h : IsIntegral R ((algebraMap R B) x)
⊢ (algebraMap A B) (mk' A ((algebraMap R B) x) h) = (algebraMap A B) ((algebraMap R A) x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra A S
inst✝ : Algebra R S
f : B ≃ₐ[R] S
h : ∀ (x : A), (algebraMap A S) x = f ((algebraMap A B) x)
x : S
⊢ IsIntegral R x ↔ ∃ y, (algebraMap A S) y = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk' A ((algebraMap S B) 1) ⋯ = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x * y)) ⋯ = mk' A ((algebraMap S B) x) ⋯ * mk' A ((algebraMap S B) y) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
⊢ mk' A ((algebraMap S B) 0) ⋯ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ Multiset.map (⇑(algebraMap A B)) (f.aroots A) = f.aroots B

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x + y)) ⋯ = mk' A ((algebraMap S B) x) ⋯ + mk' A ((algebraMap S B) y) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ ⇑(algebraMap A B) '' 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
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x : R
⊢ mk' A ((algebraMap S B) ((algebraMap R S) x)) ⋯ = (algebraMap R A) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
⊢ (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegral

Tactic:
by

Goal state after: