Instances on residue fields

instance instIsSeparableResidueFieldOfQuotientIdeal {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsMaximal] (q : Ideal B) [q.IsMaximal] [q.LiesOver p] [Algebra.IsSeparable (A ⧸ p) (B ⧸ q)] : Algebra.IsSeparable p.ResidueField q.ResidueField

instance instIsSeparableQuotientIdealOfResidueField {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) [p.IsMaximal] (q : Ideal B) [q.IsMaximal] [q.LiesOver p] [Algebra.IsSeparable p.ResidueField q.ResidueField] : Algebra.IsSeparable (A ⧸ p) (B ⧸ q)

theorem Algebra.isSeparable_residueField_iff {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} [p.IsMaximal] {q : Ideal B} [q.IsMaximal] [q.LiesOver p] : Algebra.IsSeparable p.ResidueField q.ResidueField ↔ Algebra.IsSeparable (A ⧸ p) (B ⧸ q)