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