ringOfIntegersWithValEquiv — Mathlib

English

For v a valuation on ℚ, the ring of integers of WithVal v is isomorphic to ℤ.

Русский

Для v — оценка на ℚ, кольцо целых WithVal v изоморфно ℤ.

LaTeX

$$$\mathcal{O}(WithVal v) \cong+* \mathbb{Z}$$$

Lean4

/-- The ring of integers of `WithVal v`, when `v` is a valuation on `ℚ`, is
equivalent to `ℤ`. -/
@[simps! apply]
def ringOfIntegersWithValEquiv (v : Valuation ℚ Γ₀) : 𝓞 (WithVal v) ≃+* ℤ :=
  NumberField.RingOfIntegers.withValEquiv v ℤ

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