mul_mem_centralizer — Mathlib

English

If a and b lie in the centralizer of S, then their product lies in the centralizer of S.

Русский

Если a и b принадлежат центральизатору S, то их произведение принадлежит центральizатору S.

LaTeX

$$$ a \in \mathrm{centralizer}(S) \land b \in \mathrm{centralizer}(S) \Rightarrow ab \in \mathrm{centralizer}(S) $$$

Lean4

@[to_additive (attr := simp) add_mem_addCentralizer]
theorem mul_mem_centralizer (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : a * b ∈ centralizer S := fun g hg ↦ by
  rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]

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