Theorem: pow_sub_one_dvd_differentIdeal (FltRegular/NumberTheory/Different.lean)

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 _ _ _
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

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) _ _
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

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⁰
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

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)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ P ^ (e - 1) ∣ differentIdeal A B
Tactic:
by_cases he : e = 0
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
⊢ P ^ (e - 1) ∣ differentIdeal A B

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

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
State after:
no goals

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]
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

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 _
State after:
no goals