instResidueFieldOfLiesOver — Mathlib

English

There is an instance constructing residue field algebras when a prime lies over another and the lie-over maps exist.

Русский

Существуют конструкции полей остатка через пары идеалов и отображения lies over.

LaTeX

$$instance (p q) : Algebra p.ResidueField q.ResidueField$$

Lean4

noncomputable instance (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] :
    Algebra p.ResidueField q.ResidueField :=
  (Ideal.ResidueField.mapₐ p q Ideal.LiesOver.over).toAlgebra

Похожие утверждения