map_sub_swap

Mathlib.RingTheory.Valuation.Basic

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

English

Subtraction is symmetric with respect to swapping operands: v(x - y) = v(y - x).

Русский

Вычитание симметрично относительно перестановки слагаемых: v(x - y) = v(y - x).

LaTeX

$$$$ v(x - y) = v(y - x). $$$$

Lean4

theorem map_sub_swap (x y : R) : v (x - y) = v (y - x) :=
  Valuation.map_sub_swap v x y

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

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

Разделы

Аффилиация

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