subtype — Mathlib

English

There is a canonical ring homomorphism from a valuation subring to K, denoted subtype.

Русский

Существует каноническое кольцевое отображение из оценочного подкольца в K, обозначаемое как subtype.

LaTeX

$$$\mathrm{subtype}_R: R \to K$$$

Lean4

/-- The canonical ring homomorphism from a valuation ring to its field of fractions. -/
def subtype (R : ValuationSubring K) : R →+* K :=
  Subring.subtype R.toSubring

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