R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Algebra R S
inst✝¹ : IsNoetherian R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ finrank (R ⧸ p) (S ⧸ ↑P) ≠ 0
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Algebra R S
inst✝¹ : IsNoetherian R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ inertiaDeg (algebraMap R S) p ↑P ≠ 0
rw [inertiaDeg_algebraMap]
no goals
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain S
inst✝² : Algebra R S
inst✝¹ : IsNoetherian R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ finrank (R ⧸ p) (S ⧸ ↑P) ≠ 0
exact (FiniteDimensional.finrank_pos_iff.mpr inferInstance).ne'