map_sub_eq_of_lt_right

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#AddValuation.map_sub_eq_of_lt_right

English

If v(y) < v(x), then v(x) = v(y) when considering x − y.

Русский

Если v(y) < v(x), тогда v(x) = v(y) при разности x − y.

LaTeX

$$$$ v(x) = v(y) \\quad\\text{whenever } v(y) < v(x) \\text{ and } x - y \\text{ considered}. $$$$

Lean4

theorem map_sub_eq_of_lt_right {x y : R} (hx : v y < v x) : v (x - y) = v y :=
  map_sub_swap v x y ▸ map_sub_eq_of_lt_left v hx

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

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

Разделы

Аффилиация

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