eq_zpow_of_nonzero

Mathlib.NumberTheory.Padics.PadicNorm

URI: https://scilib.ai/kg/mathlib#padicNorm.eq_zpow_of_nonzero

← MathLib Explorer

English

The maximal ideal of ℤ_p equals the principal ideal generated by p.

Русский

Максимальный идеал ℤ_p равен порожденному p идеалу.

LaTeX

$$MaximalIdeal(ℤ_[p]) = Ideal.span{p}.$$

Lean4

/-- Unfolds the definition of the `p`-adic norm of `q` when `q ≠ 0`. -/
@[simp]
protected theorem eq_zpow_of_nonzero {q : ℚ} (hq : q ≠ 0) : padicNorm p q = (p : ℚ) ^ (-padicValRat p q) := by
  simp [hq, padicNorm]

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

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

Разделы

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

Аффилиация

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