internlm/Lean-Github huggingface dataset:
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof state before:
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
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✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP✝ : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (Algebra.trace K L) ((algebraMap B L) z) ∈ ↑p
Tactic:
rw [← Algebra.algebraMap_intTrace (A := A)]
Proof state after:
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
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✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP✝ : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (algebraMap A K) ((intTrace A B) z) ∈ ↑p
Theorem: pow_sub_one_dvd_differentIdeal_aux
Proof state before:
A : Type u_2
K : Type ?u.19134
L : Type ?u.19140
B : Type u_1
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✝¹⁵ : IsDomain A
inst✝¹⁴ : IsDomain B
inst✝¹³ : IsFractionRing A K
inst✝¹² : IsIntegralClosure B A L
inst✝¹¹ : IsFractionRing B L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : IsSeparable K L
inst✝⁸ : IsIntegrallyClosed A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : IsFractionRing B L
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsFractionRing B L
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP✝ : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑(P ^ (e - 1)))⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (algebraMap A K) ((intTrace A B) z) ∈ ↑p
Tactic:
exact ⟨intTrace A B z, this z hz, rfl⟩
Proof state after:
no goals
Theorem: pow_sub_one_dvd_differentIdeal
Proof state before:
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have : IsIntegralClosure B A (FractionRing B) :=
  IsIntegralClosure.of_isIntegrallyClosed _ _ _
Proof state after:
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this : IsIntegralClosure B A (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal
Proof state before:
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this : IsIntegralClosure B A (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
  IsIntegralClosure.isLocalization _ (FractionRing A) _ _
Proof state after:
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal
Proof state before:
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
have : FiniteDimensional (FractionRing A) (FractionRing B) :=
  Module.Finite_of_isLocalization A B _ _ A⁰
Proof state after:
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal
Proof state before:
case neg
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : ¬e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) B P e he hp hP
Proof state after:
no goals
Theorem: pow_sub_one_dvd_differentIdeal
Proof state before:
case pos
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
rw [he, pow_zero]
Proof state after:
case pos
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ 1 ∣ differentIdeal A B
Theorem: pow_sub_one_dvd_differentIdeal
Proof state before:
case pos
A : Type u_1
K : Type ?u.64635
L : Type ?u.64641
B : Type u_2
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✝¹⁷ : IsDomain A
inst✝¹⁶ : IsDomain B
inst✝¹⁵ : IsFractionRing A K
inst✝¹⁴ : IsIntegralClosure B A L
inst✝¹³ : IsFractionRing B L
inst✝¹² : FiniteDimensional K L
inst✝¹¹ : IsSeparable K L
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDedekindDomain B
inst✝⁸ : IsFractionRing B L
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : NoZeroSMulDivisors A B
inst✝² : Module.Finite A B
inst✝¹ : IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ 1 ∣ differentIdeal A B
Tactic:
exact one_dvd _
Proof state after:
no goals
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Tactic:
have : Fact (p : ℕ).Prime := ⟨hp⟩
Proof state after:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Tactic:
obtain ⟨a, ha⟩ := exists_int_sub_pow_prime_dvd p α
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : α ^ ↑p - ↑a ∈ Ideal.span {↑↑p}
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : α ^ ↑p - ↑a ∈ Ideal.span {↑↑p}
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Tactic:
rw [Ideal.mem_span_singleton] at ha ⊢
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : ↑↑p ∣ α ^ ↑p - ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : ↑↑p ∣ α ^ ↑p - ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Tactic:
obtain ⟨γ, hγ⟩ := ha
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p - ↑a = ↑↑p * γ
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p - ↑a = ↑↑p * γ
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Tactic:
rw [sub_eq_iff_eq_add] at hγ
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Tactic:
rw [hγ, _root_.map_add, _root_.map_mul, map_natCast, map_intCast, add_sub_add_right_eq_sub,
  ← mul_sub]
Proof state after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ ↑↑p * (γ - (intGal ↑(galConj K p)) γ)
Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem
Proof state before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ ↑↑p * (γ - (intGal ↑(galConj K p)) γ)
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑x + ↑y * ↑(hζ.unit' ^ (-i))
Tactic:
ext1
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑((intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i))) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑((intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i))) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
Tactic:
rw [intGal_apply_coe]
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑(galConj K p) ↑(↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑(galConj K p) ↑(↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
Tactic:
simp only [_root_.map_add, map_intCast, _root_.map_mul, AlgHom.coe_coe, zpow_neg, map_units_inv,
  add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero]
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i)) = ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i))⁻¹ ∨ y = 0
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i)) = ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i))⁻¹ ∨ y = 0
Tactic:
simp_rw [NumberField.Units.coe_zpow]
Proof state after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹ ∨ y = 0
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹ ∨ y = 0
Tactic:
left
Proof state after:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹
Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux
Proof state before:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹
Tactic:
push_cast
Proof state after:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) (ζ ^ i) = (ζ ^ i)⁻¹