one_apply_lt_one_iff

Mathlib.RingTheory.Valuation.Basic

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

← MathLib Explorer

English

For a nontrivial Γ₀, the unit valuation satisfies: (1) x < 1 iff x is zero, equivalently the other form of lt-one.

Русский

Для ненулевой группы Γ₀: (1) x < 1 эквивалентно x = 0.

LaTeX

$$$ (1 : \\mathrm{Valuation}(R,\\Gamma_0))\\;x < 1 \\iff x = 0 $$$

Lean4

@[simp]
theorem one_apply_lt_one_iff [Nontrivial Γ₀] {x : R} : (1 : Valuation R Γ₀) x < 1 ↔ x = 0 :=
  by
  rw [one_apply_def]
  split_ifs <;> simp_all

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

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

Разделы

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

Аффилиация

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