mahlerEquiv_symm_apply

Mathlib.NumberTheory.Padics.MahlerBasis

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

English

The p-adic integers ℤ_p are the subspace of ℚ_p consisting of elements with norm ≤ 1.

Русский

p-адические целые ℤ_p — это подмножество ℚ_p, состоящее из элементов с нормой ≤ 1.

LaTeX

$$$$ \\mathbb{Z}_p = \\{ x \\in \\mathbb{Q}_p : \\|x\\| \\le 1 \\}. $$$$

Lean4

theorem mahlerEquiv_symm_apply (a : C₀(ℕ, E)) : (mahlerEquiv E).symm a = (mahlerSeries (p := p) a) :=
  rfl

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

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

Разделы

Аффилиация

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