unitCoeff_coe

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The coe form of unitCoeff hx coincides with x's coefficient in the rational embedding.

Русский

Коэффициент перехода unitCoeff hx совпадает с коэффициентом x в рациональном вложении.

LaTeX

$$(unitCoeff hx : \mathbb{Q}_{p}) = x * (p)^{(-x.valuation)}$$

Lean4

@[simp]
theorem unitCoeff_coe {x : ℤ_[p]} (hx : x ≠ 0) : (unitCoeff hx : ℚ_[p]) = x * (p : ℚ_[p]) ^ (-x.valuation : ℤ) :=
  rfl

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

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

Разделы

Аффилиация

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