v_p_lt_val

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#ModP.v_p_lt_val

← MathLib Explorer

English

preVal(x) = 0 iff x = 0 in ModP O p.

Русский

preVal(x) = 0 эквивалентно x = 0 в ModP O p.

LaTeX

$$$\mathrm{preVal}(x) = 0 \iff x = 0$$$

Lean4

theorem v_p_lt_val {x : O} : v p < v (algebraMap O K x) ↔ (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := by
  rw [lt_iff_not_ge, not_iff_not, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton]

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

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

Разделы

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

Аффилиация

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