centralizer_le

Mathlib.GroupTheory.Submonoid.Centralizer

URI: https://scilib.ai/kg/mathlib#Submonoid.centralizer_le

English

If S ⊆ T, then the centralizer of T is contained in the centralizer of S.

Русский

Если S ⊆ T, то центральizer(T) ⊆ centralizer(S).

LaTeX

$$$ S \subseteq T \implies \operatorname{centralizer}(T) \subseteq \operatorname{centralizer}(S) $$$

Lean4

@[to_additive]
theorem centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
  Set.centralizer_subset h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru