mem_inv_smul_finset_iff

Mathlib.Algebra.Group.Action.Pointwise.Finset

URI: https://scilib.ai/kg/mathlib#Finset.mem_inv_smul_finset_iff

English

For all a, b, Finset s, b ∈ a⁻¹ • s if and only if a • b ∈ s.

Русский

Для всех a, b, Finset s: b ∈ a⁻¹ • s тогда и только если a • b ∈ s.

LaTeX

$$$b \\in a^{-1} \\cdot s \\iff a \\cdot b \\in s$$$

Lean4

@[to_additive]
theorem mem_inv_smul_finset_iff : b ∈ a⁻¹ • s ↔ a • b ∈ s := by rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

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

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

Разделы

Аффилиация

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