map_sub_of_left_eq_zero

Mathlib.RingTheory.Valuation.Basic

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

← MathLib Explorer

English

If h: v y < v x, then v(x - y) = v x.

Русский

Если h: v y < v x, тогда v(x - y) = v x.

LaTeX

$$$(h : v y < v x) \\Rightarrow v(x - y) = v x$$$

Lean4

theorem map_sub_of_left_eq_zero (hx : v x = 0) : v (x - y) = v y :=
  by
  by_cases hy : v y = 0
  · simpa [*] using map_sub v x y
  · simp [*, map_sub_eq_of_lt_right, zero_lt_iff]

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

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

Разделы

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

Аффилиация

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