map_neg_one

Mathlib.Algebra.Ring.Units

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

← MathLib Explorer

English

For any ring homomorphism f, the image of −1 is −1: f(−1) = −1.

Русский

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

LaTeX

$$$f(-1) = -1$$$

Lean4

protected theorem map_neg_one {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β] (f : F) :
    map (f : α →* β) (-1) = -1 := by simp only [Units.map_neg, map_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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