R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝ : Algebra R S
hRS : Algebra.IsIntegral R S
I : Ideal S
hI : IsMaximal I
⊢ IsField (R ⧸ comap (algebraMap R S) I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝ : Algebra R S
hRS : Algebra.IsIntegral R S
I : Ideal S
hI : IsMaximal I
⊢ IsMaximal (comap (algebraMap R S) I)
refine' Ideal.Quotient.maximal_of_isField _ _
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝ : Algebra R S
hRS : Algebra.IsIntegral R S
I : Ideal S
hI : IsMaximal I
this : IsPrime (comap (algebraMap R S) I)
⊢ IsField (R ⧸ comap (algebraMap R S) I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝ : Algebra R S
hRS : Algebra.IsIntegral R S
I : Ideal S
hI : IsMaximal I
⊢ IsField (R ⧸ comap (algebraMap R S) I)
haveI : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _
no goals
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝ : Algebra R S
hRS : Algebra.IsIntegral R S
I : Ideal S
hI : IsMaximal I
this : IsPrime (comap (algebraMap R S) I)
⊢ IsField (R ⧸ comap (algebraMap R S) I)
exact
  isField_of_isIntegral_of_isField (isIntegral_quotient_of_isIntegral hRS)
    algebraMap_quotient_injective (by rwa [← Quotient.maximal_ideal_iff_isField_quotient])
no goals
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I✝ J : Ideal S
inst✝ : Algebra R S
hRS : Algebra.IsIntegral R S
I : Ideal S
hI : IsMaximal I
this : IsPrime (comap (algebraMap R S) I)
⊢ IsField (S ⧸ I)
rwa [← Quotient.maximal_ideal_iff_isField_quotient]