not_isUnit_iff

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

Not is-unit is equivalent to norm less than 1.

Русский

Не единица эквивалентна норме меньше 1.

LaTeX

$$¬IsUnit(z) \iff \|z\| < 1$$

Lean4

theorem not_isUnit_iff {z : ℤ_[p]} : ¬IsUnit z ↔ ‖z‖ < 1 := by simpa using mem_nonunits

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

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

Разделы

Аффилиация

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