instance IsLocalRing.quot {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)] : IsLocalRing (R ⧸ I)

instance IsLocalHom.quotient_mk {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)] : IsLocalHom (Ideal.Quotient.mk I)

instance IsLocalHom.quotient_mkₐ {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)] [CommRing S] [Algebra S R] : IsLocalHom (Ideal.Quotient.mkₐ S I)

theorem IsLocalRing.maximalIdeal_comap_mk {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)] : Ideal.comap (Ideal.Quotient.mk I) (maximalIdeal (R ⧸ I)) = maximalIdeal R

theorem IsLocalRing.maximalIdeal_comap_mkₐ {R : Type u_1} (S : Type u_2) [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)] [CommRing S] [Algebra S R] : Ideal.comap (Ideal.Quotient.mkₐ S I) (maximalIdeal (R ⧸ I)) = maximalIdeal R

instance IsLocalHom.algebraMap_quotient {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) [Nontrivial (R ⧸ I)] {Λ : Type u_3} [CommRing Λ] [Algebra Λ R] [IsLocalHom (algebraMap Λ R)] : IsLocalHom (algebraMap Λ (R ⧸ I))

instance IsLocalHom.lift {R : Type u_1} [CommRing R] (I : Ideal R) {S : Type u_4} [I.IsTwoSided] [Semiring S] (f : R →+* S) [h : IsLocalHom f] (H : ∀ a ∈ I, f a = 0) : IsLocalHom (Ideal.Quotient.lift I f H)