delta Ideal.inertiaDeg
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
⊢ inertiaDeg (algebraMap R S₁) p (comap e P) = inertiaDeg (algebraMap R S₂) p P
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
⊢ (if hPp : comap (algebraMap R S₁) (comap e P) = p then FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) else 0) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0