mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
⊢ trace R S ∘ₗ ↑R (trace S T) = trace R T

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
⊢ IsPurelyInseparable F K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
x : S × T
⊢ (trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Free R S
inst✝² : Free R T
inst✝¹ : Module.Finite R S
inst✝ : Module.Finite R T
p : S × T
⊢ (trace R (S × T)) p = ((trace R S).coprod (trace R T)) p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ (LinearMap.BilinForm.toMatrix b) (traceForm R S) i j = (trace R S) (b i * b j)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ L.fixingSubgroup.Normal ↔ IsGalois k ↥L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔ FiniteDimensional k ↥L ∧ IsGalois k ↥L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = X ^ q ^ n - C y

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
q : ℕ
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
this :
  ∀ (F E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
    [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
⊢ ∃ n, finrank F E = q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
⊢ finrank F ↥F⟮x⟯ = q ^ m

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
⊢ finrank (↥F⟮x⟯) E < d

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
n : ℕ
hn : finrank (↥F⟮x⟯) E = q ^ n
⊢ d = q ^ (m + n)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
q : ℕ
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
⊢ ∃ n, finrank F E = q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
⊢ IsPurelyInseparable F E

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ Irreducible p ↔ Irreducible (map (algebraMap R K) p)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : IsPurelyInseparable F E
L : Type u_2
inst✝¹ : CommRing L
inst✝ : IsReduced L
f g : E →+* L
heq : (fun f ↦ f.comp (algebraMap F E)) f = (fun f ↦ f.comp (algebraMap F E)) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : IsPurelyInseparable F E
L : Type w
inst✝² : CommRing L
inst✝¹ : IsReduced L
inst✝ : Algebra F L
f g : E →ₐ[F] L
⊢ (fun f ↦ f.comp (algebraMap F E)) ↑f = (fun f ↦ f.comp (algebraMap F E)) ↑g

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsPurelyInseparable F E
⊢ sepDegree F E = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
h_dvd : map (algebraMap R K) p ∣ map (algebraMap R K) q
⊢ p ∣ q

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsPurelyInseparable F E
⊢ insepDegree F E = Module.rank F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsPurelyInseparable F E ↔ Subsingleton (Emb F E)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ Algebra.IsSeparable F K ↔ finInsepDegree F K = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type w
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsPurelyInseparable F E
x : E
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type w
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F E
x : E
⊢ IsIntegral (↥(separableClosure F E)) x ∧
    (IsSeparable (↥(separableClosure F E)) x → x ∈ (algebraMap (↥(separableClosure F E)) E).range)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable (↥L) E
x : E
hx : x ∈ separableClosure F E
⊢ x ∈ L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
⊢ separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
⊢ L = separableClosure F E → Algebra.IsSeparable F ↥L ∧ IsPurelyInseparable (↥L) E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
⊢ (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑f) = (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑g)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
⊢ IsPurelyInseparable F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
⊢ IsSepClosed F

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝ : x ∈ ⊤
⊢ x ∈ adjoin E ↑(separableClosure F K)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
⊢ adjoin E ↑(separableClosure F K) = separableClosure E K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
⊢ ∀ {a b : A},
    a ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} →
      b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} → a * b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS}

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
⊢ ∀ {a b : A},
    a ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} →
      b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} → a + b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
⊢ IsLocalization (algebraMapSubmonoid C A⁰) L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ^ p ^ 0 ∈ (algebraMap R A).rangeS

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ (algebraMap R (R ⊗[k] K)) 0 = 0 ^ q ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra.IsSeparable K L
ι : Type u_5
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (b i)
inst✝ : IsIntegrallyClosed A
⊢ (↑A (Algebra.linearMap C L)).range ≤ Submodule.span A (Set.range ⇑((traceForm K L).dualBasis ⋯ b))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
L : Type u_3
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra.IsSeparable K L
ι : Type u_5
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (b i)
inst✝ : IsIntegrallyClosed A
⊢ Subalgebra.toSubmodule (integralClosure A L) ≤ Submodule.span A (Set.range ⇑((traceForm K L).dualBasis ⋯ b))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
⊢ (algebraMap A L) y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : (algebraMap k K) a = y ^ q ^ n
⊢ (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = (x ^ q ^ n) ⊗ₜ[k] 1 * 1 ⊗ₜ[k] (y ^ q ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
⊢ ∃ s b, ∀ (x : ↥s), IsIntegral A (b x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
⊢ IsNoetherian A C

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
⊢ Module.Finite A C

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : IsTorsionFree A L
⊢ finrank A C = finrank K L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
x : R ⊗[k] K
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
x : R ⊗[k] K
⊢ ∃ n > 0, x ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
m₁✝ m₂✝ : H
h : ∀ (a : B), m₁✝ • a = m₂✝ • a
⊢ ∀ (a : B), e m₁✝ • a = e m₂✝ • a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
x : H
a : A
b : B
⊢ x • a • b = a • x • b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
b : B
h : ∀ (g : H), g • b = b
g : G
x : B
⊢ e.symm g • x = g • x

Tactic:
by

Goal state after: