map_sub_of_right_eq_zero

Mathlib.RingTheory.Valuation.Basic

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

English

If v y = 0, then v(x - y) = v x.

Русский

Если v y = 0, то v(x - y) = v x.

LaTeX

$$$v(y) = 0 \\Rightarrow v(x - y) = v(x)$$$

Lean4

theorem map_sub_of_right_eq_zero (hy : v y = 0) : v (x - y) = v x := by rw [map_sub_swap, map_sub_of_left_eq_zero v hy]

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

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

Разделы

Аффилиация

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