mem_inv_pointwise_smul_iff

Mathlib.Algebra.GroupWithZero.Subgroup

URI: https://scilib.ai/kg/mathlib#AddSubgroup.mem_inv_pointwise_smul_iff

English

For any a and S, x ∈ a⁻¹ • S ⇔ a • x ∈ S.

Русский

Для любого a и подгруппы S верно x ∈ a⁻¹ • S ⇔ a • x ∈ S.

LaTeX

$$$ x \\in a^{-1} \\cdot S \\iff a \\cdot x \\in S $$$

Lean4

theorem mem_inv_pointwise_smul_iff : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
  mem_inv_smul_set_iff

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

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

Разделы

Аффилиация

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