closure_le_centralizer_centralizer

English

The same as above: the closure of a pairwise commuting set is a commutative monoid.

Русский

То же самое: замыкание пары коммутативного множества образует коммутативный моноид.

LaTeX

$$Abbrev of closureCommMonoidOfComm: closure(S) is a CommMonoid when S is pairwise commuting.$$

Lean4

@[to_additive]
theorem closure_le_centralizer_centralizer (s : Set M) : closure s ≤ centralizer (centralizer s) :=
  closure_le.mpr Set.subset_centralizer_centralizer

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