map_sub

Mathlib.Algebra.Ring.Equiv

URI: https://scilib.ai/kg/mathlib#RingEquiv.map_sub

English

Ring equivalences preserve subtraction: f(x - y) = f x - f y.

Русский

Кольцевые эквивалентности сохраняют вычитание: f(x - y) = f x - f y.

LaTeX

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

Lean4

protected theorem map_sub : f (x - y) = f x - f y :=
  map_sub f x y

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

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

Разделы

Аффилиация

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