neg_mem_center — Mathlib

English

If a is central in a nonunital nonassociative ring M, then its additive inverse −a is also central.

Русский

Если a лежит в центре неединообразной кольцевой структуры M, то −a тоже лежит в центре.

LaTeX

$$(a ∈ Center(M)) ⇒ (−a) ∈ Center(M)$$

Lean4

@[simp]
theorem neg_mem_center [NonUnitalNonAssocRing M] {a : M} (ha : a ∈ Set.center M) : -a ∈ Set.center M
    where
  comm _ := by rw [commute_iff_eq, ← neg_mul_comm, ← ha.comm, neg_mul_comm]
  left_assoc _ _ := by rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]
  right_assoc _ _ := by rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]

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