mk_coe

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.mk_coe

English

Every element k of the p-adic integers is equal to the canonical coerced element ⟨k, k.2⟩.

Русский

Любой элемент k п-адических целых равен каноническому приведённому элементу ⟨k, k.2⟩.

LaTeX

$$$(\langle k, k.2 \rangle : \mathbb{Z}_p) = k$$$

Lean4

theorem mk_coe (k : ℤ_[p]) : (⟨k, k.2⟩ : ℤ_[p]) = k := by simp

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

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

Разделы

Аффилиация

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