centralizer_centralizer_centralizer

English

The centralizer of the centralizer of s equals the centralizer of s; that is, centralizer(centralizer(centralizer(s))) = centralizer(s).

Русский

Централизатор централизатора множества s равен централизатору самого s: centralizer(centralizer(centralizer(s))) = centralizer(s).

LaTeX

$$$\\operatorname{centralizer}(\\operatorname{centralizer}(\\operatorname{centralizer}(s))) = \\operatorname{centralizer}(s)$$$

Lean4

@[simp]
theorem centralizer_centralizer_centralizer {R} [Semiring R] {s : Set R} :
    centralizer s.centralizer.centralizer = centralizer s :=
  by
  apply SetLike.coe_injective
  simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

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