mem_nonunits

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.mem_nonunits

English

An element z is in the nonunits if and only if its norm is less than 1.

Русский

Элемент z принадлежит к неединицам тогда и только тогда, когда его норма меньше 1.

LaTeX

$$z \in nonunits(\mathbb{Z}_{p}) \iff \|z\| < 1$$

Lean4

theorem mem_nonunits {z : ℤ_[p]} : z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1 := by simp [norm_le_one z, nonunits, isUnit_iff]

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

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

Разделы

Аффилиация

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