eq_zero_of_not_dvd

Mathlib.NumberTheory.Padics.PadicVal.Basic

URI: https://scilib.ai/kg/mathlib#padicValNat.eq_zero_of_not_dvd

English

If p does not divide n, then padicValNat p n = 0.

Русский

Если p не делит n, то padicValNat p n = 0.

LaTeX

$$padicValNat(p,n) = 0 \quad \text{if } ¬(p \mid n)$$

Lean4

theorem eq_zero_of_not_dvd {n : ℕ} (h : ¬p ∣ n) : padicValNat p n = 0 :=
  eq_zero_iff.2 <| Or.inr <| Or.inr h

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

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

Разделы

Аффилиация

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