norm_eq_of_norm_sub_lt_left

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

For z ∈ ℤ, ‖z.cast‖_p = 1 iff gcd(z,p) = 1.

Русский

Для z ∈ ℤ, ‖z.cast‖_p = 1 тогда и только тогда, когда gcd(z,p) = 1.

LaTeX

$$$‖z.cast‖_p = 1 \\iff \\gcd(z,p) = 1$$$

Lean4

theorem norm_eq_of_norm_sub_lt_left {z1 z2 : ℚ_[p]} (h : ‖z1 - z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖ :=
  by
  rw [eq_comm]
  apply norm_eq_of_norm_sub_lt_right
  simpa [← norm_neg (z1 - _)] using h

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

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

Разделы

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

Аффилиация

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