map_neg_one

Mathlib.Algebra.Order.Ring.Basic

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

English

For any ring hom f, f(-1) = 1.

Русский

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

LaTeX

$$$\forall f:\, \text{RingHom},\ f(-1) = 1.$$$

Lean4

theorem map_neg_one : f (-1) = 1 :=
  (pow_eq_one_iff (Nat.succ_ne_zero 1)).1 <| by rw [← map_pow, neg_one_sq, map_one]

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

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

Разделы

Аффилиация

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