nonzero

Mathlib.NumberTheory.Padics.PadicNorm

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

← MathLib Explorer

English

If q ≠ 0, then padicNorm p q ≠ 0.

Русский

Если q ≠ 0, то padicNorm p q ≠ 0.

LaTeX

$$$ padicNorm\ p\ q \neq 0 $$$

Lean4

/-- If `q ≠ 0`, then `padicNorm p q ≠ 0`. -/
protected theorem nonzero {q : ℚ} (hq : q ≠ 0) : padicNorm p q ≠ 0 :=
  by
  rw [padicNorm.eq_zpow_of_nonzero hq]
  apply zpow_ne_zero
  exact mod_cast ne_of_gt hp.1.pos

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

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

Разделы

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

Аффилиация

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