instCoeHeadWithVal

Mathlib.Topology.Algebra.Valued.WithVal

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.instCoeHeadWithVal

English

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

Русский

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

LaTeX

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

Lean4

instance : CoeHead (𝓞 (WithVal v)) (WithVal v) :=
  inferInstanceAs (CoeHead (𝓞 K) K)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru