instCharZero

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The p-adic integers ℤ_p have characteristic zero.

Русский

У п-адических целых характеристика ноль (нулевая характеристика).

LaTeX

$$$\text{CharZero}(\mathbb{Z}_p)$$$

Lean4

instance : CharZero ℤ_[p] where
  cast_injective m n h := Nat.cast_injective (R := ℚ_[p]) (by rw [Subtype.ext_iff] at h; norm_cast at h)

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

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

Разделы

Аффилиация

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