div_mem_centralizer — Mathlib

English

Let S be a subset of a group G and a,b ∈ centralizer(S). Then a/b ∈ centralizer(S); i.e., the centralizer of S is closed under division.

Русский

Пусть S — подмножество группы G и a,b принадлежат центральизатору S. Тогда a/b ∈ centralizer(S); то есть центральизатор замкнут относительно деления.

LaTeX

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

Lean4

@[to_additive (attr := simp) sub_mem_addCentralizer]
theorem div_mem_centralizer (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : a / b ∈ centralizer S := by
  simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer hb)

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