valuation_pow

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

For any x and n, the valuation of x^n is n times the valuation of x.

Русский

Для любого x и n v(x^n) = n v(x).

LaTeX

$$valuation(x^n) = n \cdot valuation(x)$$

Lean4

@[simp]
theorem valuation_pow (x : ℤ_[p]) (n : ℕ) : (x ^ n).valuation = n * x.valuation := by zify; simp [← valuation_coe]

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

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

Разделы

Аффилиация

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