div_mem_centralizer₀ — Mathlib

English

If a and b both commute with every element of s, then a/b also commutes with every element of s.

Русский

Если a и b оба коммутируют с каждым элементом s, то a/b тоже коммутирует с каждым элементом s.

LaTeX

$$$a \in centralizer(s) \land b \in centralizer(s) \Rightarrow a/b \in centralizer(s)$$$

Lean4

@[simp]
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)

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