subset_pointwise_smul_iff

Mathlib.Algebra.Group.Subgroup.Pointwise

URI: https://scilib.ai/kg/mathlib#Subgroup.subset_pointwise_smul_iff

English

Equality of two subgroupOf constructions under conj, as in conj_smul_subgroupOf.

Русский

Равенство двух конструируемых через сопряжение подгрупп внутри H.

LaTeX

$$$ {P \; H : Subgroup G} \; (hP : P \le H) (h : H) :\ldots $$$

Lean4

theorem subset_pointwise_smul_iff {a : α} {S T : Subgroup G} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
  subset_smul_set_iff

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

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

Разделы

Аффилиация

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