Algebraic extensions of the residue field

instance instIsAlgebraicQuotientIdealResidueField {R : Type u_1} [CommRing R] (p : Ideal R) [p.IsPrime] : Algebra.IsAlgebraic (R ⧸ p) p.ResidueField

instance instIsAlgebraicResidueFieldOfIsIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [p.IsPrime] [P.IsPrime] [P.LiesOver p] [Algebra.IsIntegral R S] : Algebra.IsAlgebraic p.ResidueField P.ResidueField