centralizer_univ — Mathlib

English

The centralizer of Set.univ equals the center: centralizer(R, Set.univ) = center(R,A).

Русский

Централизатор множества всех элементов равен центру: centralizer(R, Set.univ) = center(R,A).

LaTeX

$$$\operatorname{centralizer}(R,\mathrm{Set.univ}) = \operatorname{center}(R,A)$$$

Lean4

@[simp]
theorem centralizer_univ : centralizer R Set.univ = center R A :=
  SetLike.ext' <| by rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]

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