int_lt_one_iff

Mathlib.NumberTheory.Padics.PadicNorm

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

← MathLib Explorer

English

For an integer 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 int_lt_one_iff (m : ℤ) : padicNorm p m < 1 ↔ (p : ℤ) ∣ m :=
  by
  rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt]
  simp only [padicNorm.of_int, true_and]

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

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

Разделы

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

Аффилиация

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