mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Field S
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra K S
inst✝⁴ : Algebra L S
inst✝³ : IsScalarTower K L S
inst✝² : Normal K L
inst✝¹ : DecidableEq L
inst✝ : Fintype Gal(L/K)
c : ConjRootClass K L
x x✝ : L
⊢ x✝ ∈ Finset.image (fun x_1 ↦ x_1 x) Finset.univ ↔ x✝ ∈ carrier ⟦x⟧

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c d : ConjRootClass K L
⊢ c.minpoly = d.minpoly ↔ c = d

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
n : Normal K L
c : ConjRootClass K L
⊢ (map (algebraMap K L) c.minpoly).Splits

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ c.minpoly.Monic

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ Irreducible c.minpoly

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x : L
c : ConjRootClass K L
⊢ (aeval x) c.minpoly = 0 ↔ mk K x = c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Flat R ↥A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥A = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ c.minpoly.rootSet L = c.carrier

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
c : ConjRootClass K L
⊢ c.minpoly.Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = c.carrier.toFinset.val

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.carrier.toFinset = { val := c.minpoly.aroots L, nodup := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ map (algebraMap K L) c.minpoly = ∏ x ∈ c.carrier.toFinset, (X - C x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.trace (↥A) S) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.trace R ↥B) x)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
f : E →ₐ[F] K
a : E
⊢ normalizedTraceAux F K (f a) = normalizedTraceAux F E a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) S) x) = (algebraMap R ↥A) ((Algebra.norm R) x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
A : Type v
inst✝⁶ : CommRing A
B : Type w
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Flat R A
inst✝¹ : Flat R B
inst✝ : IsDomain (A ⊗[R] B)
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
K : Type (max w v) := FractionRing (A ⊗[R] B)
i : A ⊗[R] B →ₐ[R] K := IsScalarTower.toAlgHom R (A ⊗[R] B) K
hi : Function.Injective ⇑i
⊢ (i.comp Algebra.TensorProduct.includeLeft).range.LinearDisjoint (i.comp Algebra.TensorProduct.includeRight).range

Tactic:
simpa only [AlgHom.range_comp] using (include_range R A B).map i hi

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : FiniteDimensional F K
a : K
⊢ normalizedTraceAux F K a = (↑(Module.finrank F K))⁻¹ • (trace F K) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
A : Type v
inst✝⁶ : CommRing A
B : Type w
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Flat R A
inst✝¹ : Flat R B
inst✝ : IsDomain (A ⊗[R] B)
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
K : Type (max w v) := FractionRing (A ⊗[R] B)
i : A ⊗[R] B →ₐ[R] K := IsScalarTower.toAlgHom R (A ⊗[R] B) K
hi : Function.Injective ⇑i
⊢ (i.comp Algebra.TensorProduct.includeLeft).range.LinearDisjoint (i.comp Algebra.TensorProduct.includeRight).range

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ A.LinearDisjoint ↥B ↔ A.LinearDisjoint B.toSubalgebra

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
H : IsField (↥A ⊗[R] ↥B)
⊢ A.LinearDisjoint B

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type v
inst✝³ : Ring A
B : Type w
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
⊢ fa.range.LinearDisjoint fb.range

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

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✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L'
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (r : L), (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) r = 0 → r = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • x✝) =
    x✝¹ • (AddMonoidHom.id E) x✝

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
⊢ normalizedTraceAux F K (m • a) = (RingHom.id F) m • normalizedTraceAux F K a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ (normalizedTrace F F) a = a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹⁰ : Field F
inst✝⁹ : Field E
inst✝⁸ : Field K
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra E K
inst✝⁵ : Algebra F K
inst✝⁴ : IsScalarTower F E K
inst✝³ : Algebra.IsIntegral F K
inst✝² : CharZero F
inst✝¹ : CharZero E
inst✝ : Algebra.IsIntegral E K
a : K
h : minpoly E a ∈ Polynomial.lifts (algebraMap F E)
⊢ (algebraMap F E) ((normalizedTrace F K) a) = (normalizedTrace E K) a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) (x✝¹ • x✝) =
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • (AddMonoidHom.id E) x✝

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
b : ι → L
hb : LinearIndependent F b
⊢ LinearIndependent (↥A) (⇑(algebraMap L E) ∘ b)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
κ : Type u_1
ι : Type u_2
a : κ → ↥A
b : ι → L
ha : LinearIndependent F a
hb : LinearIndependent F b
⊢ LinearIndependent F fun i ↦ ↑(a i.1) * (algebraMap L E) (b i.2)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ A.LinearDisjoint L'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
H : A.LinearDisjoint ↥B
⊢ finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
H : finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B
⊢ finrank F ↥(A.toSubalgebra ⊔ B.toSubalgebra) = finrank F ↥A.toSubalgebra * finrank F ↥B.toSubalgebra

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
⊢ (normalizedTrace F E) ((normalizedTrace E K) a) = (normalizedTrace F K) a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a : F
⊢ (normalizedTrace F K) ((algebraMap F K) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimeField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
⊢ ⊥ = (algebraMap ℚ K).fieldRange

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimeField

Goal state before:
pp: K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
⊢ ⊥ = (algebraMap (ZMod p) K).fieldRange

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
x : k
⊢ (root k) x ^ p = (algebraMap k (AdjoinPthRoots k)) x

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
x : AdjoinPthRoots k
⊢ (algebraMap k (AdjoinPthRoots k)) ((root k).symm x) = x ^ p

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
⊢ IsPurelyInseparable k (AdjoinPthRoots k)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : Module.Finite F ↥A
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
⊢ finrank (↥A) E = finrank F ↥B

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : Module.Finite F ↥B
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
⊢ B ⊔ A = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ fa a = a ⊗ₜ[R] 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
⊢ ↥⊥ ⊗[R] ↥A ≃ₐ[R] ↥A

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : IsGalois F ↥A
inst✝ : FiniteDimensional F E
h₁ : A ⊔ B = ⊤
h₂ : A ⊓ B = ⊥
⊢ A.LinearDisjoint ↥B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
⊢ ↥A ⊗[R] ↥⊥ ≃ₐ[R] ↥A

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : CommRing K
inst✝² : Ring L
inst✝¹ : Algebra K L
inst✝ : HasExponent K L
a : L
⊢ a ^ ringExpChar K ^ exponent K L ∈ (algebraMap K L).range

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : CommRing K
inst✝² : Ring L
inst✝¹ : Algebra K L
inst✝ : HasExponent K L
e : ℕ
h : e < exponent K L
⊢ ∃ a, a ^ ringExpChar K ^ e ∉ (algebraMap K L).range

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
⊢ ∀ (x : ↥includeLeft.range) (y : ↥includeRight.range),
    (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict ∘ₗ
          includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range)
        (x ⊗ₜ[R] y) =
      LinearMap.id (x ⊗ₜ[R] y)

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
h : a ∈ (algebraMap K L).range
⊢ elemExponent K a = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ minpoly K a = X ^ ringExpChar K ^ elemExponent K a - C (elemReduct K a)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range ∘ₗ
        _root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
      (x ⊗ₜ[R] y) =
    LinearMap.id (x ⊗ₜ[R] y)

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ (minpoly K a).natDegree = ringExpChar K ^ elemExponent K a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
⊢ ∀ (a₁ a₂ : S) (b₁ b₂ : T),
    (linearEquivIncludeRange R S T) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (linearEquivIncludeRange R S T) (a₁ ⊗ₜ[R] b₁) * (linearEquivIncludeRange R S T) (a₂ ⊗ₜ[R] b₂)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
⊢ ((map f A).mulMap (map f B)).comp (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) =
    f.comp (A.mulMap B)

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ B.mulMap A = (A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ (A.mulMap B).range = A ⊔ B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Surjective ⇑(A.mulMap' B)

Tactic:
mulMap',

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Surjective ⇑((↑((A.mulMap B).range.equivOfEq (A ⊔ B) ⋯)).comp (A.mulMap B).rangeRestrict)