padicValInt_dvd

Mathlib.NumberTheory.Padics.PadicVal.Basic

URI: https://scilib.ai/kg/mathlib#padicValInt_dvd

English

For a fixed prime p, p^{padicValInt p a} divides a for any a ∈ ℤ.

Русский

Для фиксированного простого p число p^{v_p(a)} делит a для любого a ∈ ℤ.

LaTeX

$$$\\forall a \\in \\mathbb{Z},\\ (p : \\mathbb{Z})^{\\operatorname{padicValInt} p a} \\mid a$$$

Lean4

theorem padicValInt_dvd (a : ℤ) : (p : ℤ) ^ padicValInt p a ∣ a :=
  by
  rw [padicValInt_dvd_iff]
  exact Or.inr le_rfl

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

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

Разделы

Аффилиация

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