nat_lt_one_iff

Mathlib.NumberTheory.Padics.PadicNorm

URI: https://scilib.ai/kg/mathlib#padicNorm.nat_lt_one_iff

English

For a natural m, padicNorm p m < 1 if and only if p divides m.

Русский

Для натурального m: padicNorm p m < 1 тогда и только тогда, когда p делит m.

LaTeX

$$$ padicNorm\ p\ m < 1 \iff p \mid m $$$

Lean4

theorem nat_lt_one_iff (m : ℕ) : padicNorm p m < 1 ↔ p ∣ m := by
  rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]

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

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

Разделы

Аффилиация

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