ne_zero_of_isUnit

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.ne_zero_of_isUnit

← MathLib Explorer

English

If u is a unit, then v(u) ≠ 0.

Русский

Если u гамUnit, то v(u) ≠ 0.

LaTeX

$$$ v(u) \neq 0 $$$

Lean4

theorem ne_zero_of_isUnit [Nontrivial Γ₀] (v : Valuation K Γ₀) (x : K) (hx : IsUnit x) : v x ≠ (0 : Γ₀) := by
  simpa [hx.choose_spec] using ne_zero_of_unit v hx.choose

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

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

Разделы

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

Аффилиация

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