mathlib-initiative/mathlib-tactics huggingface dataset:
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
he' : ∀ (g : G) (x : B), e.symm g • x = g • x
g : G
⊢ g • b = 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
he' : ∀ (g : G) (x : B), e.symm g • x = g • x
g : G
⊢ g • b = b

Tactic:
by simpa [he'] using h (e.symm g)

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
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
⊢ IsGaloisGroup H A B ↔ IsGaloisGroup G A 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
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
m₁✝ m₂✝ : G
h : ∀ (a : B'), m₁✝ • a = m₂✝ • a
b : B
⊢ m₁✝ • b = m₂✝ • 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
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' x' : B'
⊢ e.symm (g • x') = g • e.symm x'

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
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' : B'
⊢ g • a • b' = a • g • 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
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
g : G
⊢ g • e.symm x' = e.symm x'

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
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
a : A
ha : (algebraMap A B) a = e.symm x'
⊢ (algebraMap A B') a = x'

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
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
⊢ ∃ a, (algebraMap A B') a = x'

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
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
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
⊢ ∀ (m : G) (n : A') (a : B), m • n • a = n • m • a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
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
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
b : B
h : ∀ (g : G), g • b = b
a : A
ha : (algebraMap A B) a = b
⊢ (algebraMap A' B) (e a) = b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
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
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
⊢ ∀ (b : B), (∀ (g : G), g • b = b) → ∃ a, (algebraMap A' B) a = b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x : A
x✝ : G
⊢ x✝ • (algebraMap A B) x = (algebraMap A B) x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝ : A
⊢ (fun x ↦ ⋯.choose) ((fun x ↦ ⟨(algebraMap A B) x, ⋯⟩) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x : ↥(FixedPoints.subsemiring B G)
⊢ (fun x ↦ ⟨(algebraMap A B) x, ⋯⟩) ((fun x ↦ ⋯.choose) x) = x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝¹ x✝ : A
⊢ ⟨(algebraMap A B) (x✝¹ * x✝), ⋯⟩ = ⟨(algebraMap A B) x✝¹, ⋯⟩ * ⟨(algebraMap A B) x✝, ⋯⟩

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x✝¹ x✝ : A
⊢ ⟨(algebraMap A B) (x✝¹ + x✝), ⋯⟩ = ⟨(algebraMap A B) x✝¹, ⋯⟩ + ⟨(algebraMap A B) x✝, ⋯⟩

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁸ : Group G
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra A B
inst✝⁴ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝³ : FaithfulSMul A B
inst✝² : CommSemiring A'
inst✝¹ : Algebra A' B
inst✝ : FaithfulSMul A' B
hA' : IsGaloisGroup G A' B
x : A
⊢ (algebraMap A' B) ((ringEquiv G A A' B) x) = (algebraMap A B) x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁸ : Group G
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra A B
inst✝⁴ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝³ : FaithfulSMul A B
inst✝² : CommSemiring A'
inst✝¹ : Algebra A' B
inst✝ : FaithfulSMul A' B
hA' : IsGaloisGroup G A' B
x : A'
⊢ (algebraMap A B) ((ringEquiv G A A' B).symm x) = (algebraMap A' B) x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
B : Type u_3
inst✝⁴ : Group G
inst✝³ : Semiring B
inst✝² : MulSemiringAction G B
C : Type u_4
inst✝¹ : CommSemiring C
inst✝ : Algebra C B
N : Subgroup G
hN : N.Normal
hC : IsGaloisGroup (↥N) C B
g : G
x : C
⊢ g • (algebraMap C B) x ∈ Set.range ⇑(algebraMap C B)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : IsGaloisGroup G A B
g : G
x✝ : ↥(algebraMap A B).range
b a' : B
a : A
ha : (algebraMap A B) a = a'
⊢ g • ⟨a', ⋯⟩ • b = ⟨a', ⋯⟩ • g • b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : IsGaloisGroup G A B
b : B
hb : ∀ (g : G), g • b = b
⊢ ∃ a, (algebraMap (↥(algebraMap A B).range) B) a = b

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
a : A
⊢ (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)

Tactic:
by

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

Goal state before:
pp: case refine_1
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
m₁✝ m₂✝ : G
h : ∀ (a : B), m₁✝ • a = m₂✝ • a
this : FaithfulSMul G L
a b : B
hb : b ∈ nonZeroDivisors B
⊢ m₁✝ • ((algebraMap B L) a / (algebraMap B L) b) = m₂✝ • ((algebraMap B L) a / (algebraMap B L) b)

Tactic:
simp only [smul_div₀', ← algebraMap.coe_smul', h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ (LinearMap.BilinForm.toMatrix h.basis) (traceForm R S) = of fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ 0 < (minpoly K pb.gen).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
e : K ≃+* L
inst✝ : NumberField K
⊢ e.toAddMonoidHom 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹ : Field K
inst✝ : Field L
⊢ instAlgebra K = instAlgebra_1 K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x y : K
hx : x ∈ integralClosure ℤ K
hy : y ∈ integralClosure ℤ K
⊢ ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ⟨f ↑1, ⋯⟩ = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ⟨f ↑(x * y), ⋯⟩ = ⟨f ↑x, ⋯⟩ * ⟨f ↑y, ⋯⟩

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
x : B
h : ∀ (g : G), g • x = x
⊢ ∀ (g : G), g • (algebraMap B L) x = (algebraMap B L) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ⟨f ↑0, ⋯⟩ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ⟨f ↑(x + y), ⋯⟩ = ⟨f ↑x, ⋯⟩ + ⟨f ↑y, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : 𝓞 K
⊢ IsIntegral ℤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ¬IsField (𝓞 K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ restrict (⇑f) h 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : AddZeroClass M
f : M →+ K
h : ∀ (x : M), IsIntegral ℤ (f x)
x y : M
⊢ restrict (⇑f) h (x + y) = restrict (⇑f) h x + restrict (⇑f) h y

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
⊢ restrict (⇑f) h 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : NumberField K
M : Type u_3
inst✝ : MulOneClass M
f : M →* K
h : ∀ (x : M), IsIntegral ℤ (f x)
x y : M
⊢ restrict (⇑f) h (x * y) = restrict (⇑f) h x * restrict (⇑f) h y

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(integralBasis K)) ↔ x ∈ (algebraMap (𝓞 K) K).range

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
hc : ∀ (a : A), (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) ((algebraMap A B) a)
x : B
h : ∀ (g : G), g • x = x
a : A
hb : (algebraMap K L) ((algebraMap A K) a) = (algebraMap B L) x
⊢ (algebraMap A B) a = x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: z : 𝓞 ℚ
⊢ ↑(ringOfIntegersEquiv z) = (algebraMap (𝓞 ℚ) ℚ) z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: f : Polynomial ℚ
hf : Fact (Irreducible f)
⊢ FiniteDimensional ℚ (AdjoinRoot f)

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁸ : Group G
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : MulSemiringAction G B
inst✝¹⁴ : Algebra A B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A L
inst✝⁷ : IsFractionRing A K
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : MulSemiringAction G L
inst✝² : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsIntegral A B
⊢ IsGaloisGroup G A B

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : SMulCommClass G A B
H : Subgroup G
inst✝ : H.Normal
g : G
x : ↥(FixedPoints.subring B ↥H)
h : ↥H
⊢ h • g • ↑x = g • ↑x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : SMulCommClass G A B
H : Subgroup G
inst✝ : H.Normal
⊢ ∀ (a b : G), a ≈ b → (fun x ↦ ⟨a • ↑x, ⋯⟩) = fun x ↦ ⟨b • ↑x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
H : Subgroup G
inst✝¹ : H.Normal
inst✝ : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
⊢ ∃ a, (algebraMap A ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ charpoly G b = ∏ g, g • (X - C b)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝²² : Group G
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : MulSemiringAction G B
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A L
inst✝¹¹ : IsFractionRing A K
inst✝¹⁰ : IsFractionRing B L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : MulSemiringAction G L
inst✝⁶ : SMulDistribClass G B L
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : Finite G
inst✝² : IsGaloisGroup G A B
inst✝¹ : Algebra (FractionRing A) (FractionRing B)
inst✝ : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ IsGaloisGroup G (FractionRing A) (FractionRing B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (charpoly G b) = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝⁵ : CommRing S
K : Type u_4
inst✝⁴ : Field K
F : Type u_6
inst✝³ : Field F
inst✝² : Algebra K S
inst✝¹ : Algebra K F
inst✝ : Nontrivial S
pb : PowerBasis K S
hf : (Polynomial.map (algebraMap K F) (minpoly K pb.gen)).Splits
⊢ (algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
g : G
⊢ g • charpoly G b = charpoly G b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
n : ℕ
g : G
⊢ g • (charpoly G b).coeff n = (charpoly G b).coeff n

Tactic:
by

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

Goal state before:
pp: case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis (↥s) K ↥K⟮x⟯)

Tactic:
contrapose hx

Goal state after:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ∃ s, Nonempty (Basis (↥s) K ↥K⟮x⟯)
⊢ IsIntegral K x
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
inst✝³ : FaithfulSMul A B
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
inst✝ : Finite G
⊢ Function.Bijective ⇑(MulSemiringAction.toAlgAut G A B)

Tactic:
by

Goal state after: