add_mem_centralizer — Mathlib

English

Let S be a subset of a semiring M. If a and b lie in the centralizer of S, then a + b also lies in the centralizer of S.

Русский

Пусть S ⊆ M. Если a и b центральизуют S, то и a + b централизуют S.

LaTeX

$$(a ∈ centralizer(S)) ∧ (b ∈ centralizer(S)) ⇒ (a + b) ∈ centralizer(S)$$

Lean4

@[simp]
theorem add_mem_centralizer [Distrib M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : a + b ∈ centralizer S :=
  fun c hc => by rw [add_mul, mul_add, ha c hc, hb c hc]

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