R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hp : IsMaximal p
hQ : Subsingleton (S ⧸ P)
this : P = ⊤
⊢ inertiaDeg f p P = 0
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hp : IsMaximal p
hQ : Subsingleton (S ⧸ P)
⊢ inertiaDeg f p P = 0
have := Ideal.Quotient.subsingleton_iff.mp hQ
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
hp : IsMaximal p
hQ : Subsingleton (S ⧸ ⊤)
⊢ inertiaDeg f p ⊤ = 0
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hp : IsMaximal p
hQ : Subsingleton (S ⧸ P)
this : P = ⊤
⊢ inertiaDeg f p P = 0
subst this
no goals
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
hp : IsMaximal p
hQ : Subsingleton (S ⧸ ⊤)
⊢ inertiaDeg f p ⊤ = 0
exact dif_neg fun h => hp.ne_top <| h.symm.trans comap_top