mem_inv_pointwise_smul_iff₀

Mathlib.Algebra.GroupWithZero.Subgroup

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

English

For ha ≠ 0, x ∈ a⁻¹ • S ⇔ a • x ∈ S.

Русский

Пусть ha ≠ 0. Тогда x ∈ a⁻¹ • S ⇔ a • x ∈ S.

LaTeX

$$$ (ha \\neq 0) \\Rightarrow \\ x \\in a^{-1} \\cdot S \\iff a \\cdot x \\in S $$$

Lean4

theorem mem_inv_pointwise_smul_iff₀ (ha : a ≠ 0) (S : AddSubgroup A) (x : A) : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
  mem_inv_smul_set_iff₀ ha (S : Set A) x

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

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

Разделы

Аффилиация

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