add_mem_center — Mathlib

English

If a and b are central in a distributive semiring M, then their sum a + b is also central.

Русский

Если a и b лежат в центре M, то их сумма a + b также лежит в центре.

LaTeX

$$(a ∈ Center(M)) ∧ (b ∈ Center(M)) ⇒ (a + b) ∈ Center(M)$$

Lean4

@[simp]
theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a + b ∈ Set.center M
    where
  comm _ := by rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]
  left_assoc _ _ := by rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
  right_assoc _ _ := by rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]

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