dvd_of_one_le_padicValNat

Mathlib.NumberTheory.Padics.PadicVal.Basic

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

← MathLib Explorer

English

If a ≠ 0, then p^n divides a iff n ≤ v_p(a).

Русский

Если a ≠ 0, то p^n делит a тогда и только тогда, когда n ≤ v_p(a).

LaTeX

$$$ a \\neq 0 \\Rightarrow p^n \\mid a \\Leftrightarrow n \\le v_p(a) $$$

Lean4

theorem dvd_of_one_le_padicValNat {n : ℕ} (hp : 1 ≤ padicValNat p n) : p ∣ n :=
  by
  by_contra h
  rw [padicValNat.eq_zero_of_not_dvd h] at hp
  exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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