p_nonunit

Mathlib.NumberTheory.Padics.PadicIntegers

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

← MathLib Explorer

English

The element p is a nonunit in Z_p.

Русский

Элемент p не является единицей в Z_p.

LaTeX

$$$p \notin (\mathbb{Z}_p)^{\times}$.$$

Lean4

theorem p_nonunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p] :=
  by
  have : (p : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp.out.one_lt
  rwa [← norm_p, ← mem_nonunits] at this

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

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

Разделы

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

Аффилиация

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