WithVal — Mathlib

English

For any ring R and valuation v on R, WithVal v is just a copy of R; it is canonically isomorphic to R as a ring.

Русский

Для кольца R и оценки v на R WithVal v есть каноническое изоморфное отображение WithVal v ≅ R как кольца.

LaTeX

$$$WithVal(v) \cong R$$$

Lean4

/-- Type synonym for a ring equipped with the topology coming from a valuation. -/
@[nolint unusedArguments]
def WithVal [Ring R] : Valuation R Γ₀ → Type _ := fun _ => R

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