centralizer_le

Mathlib.GroupTheory.Subsemigroup.Centralizer

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

English

If S ⊆ T as sets, then centralizer T is contained in centralizer S.

Русский

Если S ⊆ T как множества, то centralizer(T) ⊆ centralizer(S).

LaTeX

$$$ \\text{centralizer}(T) \\le \\text{centralizer}(S) $ given $ S \\subseteq T $$$

Lean4

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

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

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

Разделы

Аффилиация

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