neg_mem_centralizer

Mathlib.Algebra.Ring.Centralizer

URI: https://scilib.ai/kg/mathlib#Set.neg_mem_centralizer

← MathLib Explorer

English

If a lies in the centralizer of S in a ring with distributive negation, then −a lies in the centralizer of S.

Русский

Если a центральизует S, то −a тоже центральизует S.

LaTeX

$$(a ∈ centralizer(S)) ⇒ (−a) ∈ centralizer(S)$$

Lean4

@[simp]
theorem neg_mem_centralizer [Mul M] [HasDistribNeg M] (ha : a ∈ centralizer S) : -a ∈ centralizer S := fun c hc => by
  rw [mul_neg, ha c hc, neg_mul]

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

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

Разделы

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

Аффилиация

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