norm_natCast_lt_one_iff

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.norm_natCast_lt_one_iff

← MathLib Explorer

English

For n ∈ ℕ, ‖n‖_p < 1 if and only if p divides n.

Русский

Для n ∈ ℕ, ‖n‖_p < 1 тогда и только тогда, когда p делит n.

LaTeX

$$$‖n‖_p < 1 \\iff p \\mid n$$$

Lean4

@[simp]
theorem norm_natCast_lt_one_iff {n : ℕ} : ‖(n : ℚ_[p])‖ < 1 ↔ p ∣ n := by
  simpa [Int.natCast_dvd_natCast] using norm_intCast_lt_one_iff (p := p) (k := n)

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

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

Разделы

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

Аффилиация

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