mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis (Free.ChooseBasisIndex A R₂) K ↥F₂ := Basis.localizationLocalization K A⁰ (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
h_main : x ∈ span R₁ (Set.range ⇑B₁.traceDual)
i j : Free.ChooseBasisIndex A R₂
⊢ (if j = i then 1 else 0) = if j = i then 1 else 0

Tactic:
]

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

Goal state before:
pp: case refine_2
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
]

Goal state after:
case refine_2
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) ↑p

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := numberField {p ^ (k + 1)} ℚ K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) ↑p
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hz : p • z ∈ (aeval B.gen).range
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
⊢ z ∈ R[B.gen]

Tactic:
]

Goal state after:
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hz : p • z ∈ (aeval B.gen).range
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
⊢ z ∈ R[B.gen]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_1
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ ζ ^ 1 = 1

Tactic:
]

Goal state after:
case refine_1
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ ζ ^ 1 = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case refine_2
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
]

Goal state after:
case refine_2
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
this : NumberField K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) (-2)

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
this : NumberField K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) (-2)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : (algebraMap R L) p = 0
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

Tactic:
]

Goal state after:
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : (algebraMap R L) p = 0
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
this : NumberField K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (n✝ + 1 + 1))
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (Int.castRingHom ℚ) 2

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
this : NumberField K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (n✝ + 1 + 1))
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (Int.castRingHom ℚ) 2
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case pos.inr
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H₁ : z = 0
⊢ 0 ∈ R[B.gen]

Tactic:
]

Goal state after:
case pos.inr
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H₁ : z = 0
⊢ 0 ∈ R[B.gen]
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n : ℕ
inst✝ : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
this✝ : NumberField K
this : NeZero n
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ p ^ s - 1)) = (algebraMap ℤ ℚ) (↑p ^ p ^ s)

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ p ^ s - 1)) = (algebraMap ℤ ℚ) (↑p ^ p ^ s)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ 2 ^ k - 1)) = (algebraMap ℤ ℚ) ((-2) ^ 2 ^ k)

Tactic:
]

Goal state after:
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
this : NumberField K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ 2 ^ k - 1)) = (algebraMap ℤ ℚ) ((-2) ^ 2 ^ k)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
⊢ p ^ (k - s).succ = 2

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
⊢ p ^ (k - s).succ = 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: k : ℕ
K : Type u_1
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 2)} ℚ K
hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))
this : NumberField K
⊢ 2 = 2

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case neg.hi.convert_2
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : Q.degree < P.degree
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n

Tactic:
]

Goal state after:
case neg.hi.convert_2
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : Q.degree < P.degree
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2} ℚ K
hζ✝ : IsPrimitiveRoot ζ 2
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ (Algebra.norm ℤ) (hζ✝.toInteger - 1) = -2

Tactic:
]

Goal state after:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2} ℚ K
hζ✝ : IsPrimitiveRoot ζ 2
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
⊢ (Algebra.norm ℤ) (hζ✝.toInteger - 1) = -2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
⊢ Prime ↑p

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
⊢ Prime ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
⊢ Prime ↑p

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
⊢ Prime ↑p
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
⊢ Q.natDegree = Q.natDegree

Tactic:
]

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
⊢ p ^ k * (p - 1) ≠ 0 ∧ p ^ k * (p - 1) ≠ 1

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
⊢ p ^ k * (p - 1) ≠ 0 ∧ p ^ k * (p - 1) ≠ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I : Submodule B L
c : B
x : L
hx : x ∈ ((traceForm K L).dualSubmodule (restrictScalars A I)).carrier
a : L
ha : a ∈ restrictScalars A I
⊢ (Algebra.trace K L) (x * c • a) ∈ 1

Tactic:
]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I : Submodule B L
c : B
x : L
hx : x ∈ ((traceForm K L).dualSubmodule (restrictScalars A I)).carrier
a : L
ha : a ∈ restrictScalars A I
⊢ (Algebra.trace K L) (x * c • a) ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ ∀ m ∈ restrictScalars A I, ∀ n ∈ restrictScalars A J, m * n ∈ comap (↑A (Algebra.trace K L)) 1

Tactic:
]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ ∀ m ∈ restrictScalars A I, ∀ n ∈ restrictScalars A J, m * n ∈ comap (↑A (Algebra.trace K L)) 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ I ≤ Jᵛ

Tactic:
]

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

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger = ↑p * x + ↑n
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
⊢ False

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger = ↑p * x + ↑n
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ J ≤ Iᵛ ↔ J ≤ Iᵛ

Tactic:
]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : CommRing B
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K L
hb : restrictScalars A I = span A (Set.range ⇑b)
⊢ (traceForm K L).dualSubmodule (span A (Set.range ⇑b)) = span A (Set.range ⇑b.traceDual)

Tactic:
]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : CommRing B
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsScalarTower A B L
inst✝³ : FiniteDimensional K L
inst✝² : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι K L
hb : restrictScalars A I = span A (Set.range ⇑b)
⊢ (traceForm K L).dualSubmodule (span A (Set.range ⇑b)) = span A (Set.range ⇑b.traceDual)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.basis ⟨1, hdim⟩ = hζ.toInteger ^ ↑⟨1, hdim⟩
⊢ False

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : 1 < pB.dim
h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.basis ⟨1, hdim⟩ = hζ.toInteger ^ ↑⟨1, hdim⟩
⊢ False