map_neg

Mathlib.Algebra.Order.Ring.Basic

URI: https://scilib.ai/kg/mathlib#MonoidHom.map_neg

English

For any MonoidHom f, f(-x) = f(x).

Русский

Для любого моноидного гомоморфизма f выполняется f(-x) = f(x).

LaTeX

$$$\forall x,\ f(-x) = f(x).$$$

Lean4

@[simp]
theorem map_neg (x : R) : f (-x) = f x := by rw [← neg_one_mul, map_mul, map_neg_one, one_mul]

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

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

Разделы

Аффилиация

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