Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Module.finrank D E = p.inertiaDegIn B
⊢ Module.finrank D E = p.inertiaDegIn B

pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : (p.primesOver B).ncard * Module.finrank D E = (p.primesOver B).ncard * p.inertiaDegIn B
⊢ (p.primesOver B).ncard ≠ 0

Tactic:
]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Module.finrank D E = p.inertiaDegIn B
⊢ Module.finrank D E = p.inertiaDegIn B

A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁸ : Field K
inst✝²⁷ : Field L
inst✝²⁶ : Algebra K L
inst✝²⁵ : CommRing A
inst✝²⁴ : CommRing B
inst✝²³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝²² : P.LiesOver p
inst✝²¹ : FiniteDimensional K L
inst✝²⁰ : MulSemiringAction Gal(L/K) B
inst✝¹⁹ : IsGaloisGroup Gal(L/K) A B
inst✝¹⁸ : IsDedekindDomain A
inst✝¹⁷ : IsDedekindDomain B
inst✝¹⁶ : Module.Finite A B
inst✝¹⁵ : Module.IsTorsionFree A B
inst✝¹⁴ : Ring.HasFiniteQuotients A
inst✝¹³ : P.IsMaximal
D : Type u_5
inst✝¹² : Field D
inst✝¹¹ : Algebra D L
inst✝¹⁰ : IsDecompositionField K L P D
E : Type u_6
inst✝⁹ : Field E
inst✝⁸ : Algebra E L
inst✝⁷ : IsInertiaField K L P E
inst✝⁶ : IsGalois K L
inst✝⁵ : Algebra K D
inst✝⁴ : Algebra K E
inst✝³ : Algebra D E
inst✝² : IsScalarTower K D E
inst✝¹ : IsScalarTower K E L
inst✝ : IsScalarTower K D L
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : (p.primesOver B).ncard * Module.finrank D E = (p.primesOver B).ncard * p.inertiaDegIn B
⊢ (p.primesOver B).ncard ≠ 0