inv_op_smul_set_distrib

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.inv_op_smul_set_distrib

← MathLib Explorer

English

For a ∈ α and s ⊆ α, (a • s)⁻¹ = a⁻¹ • s⁻¹.

Русский

Для a ∈ α и s ⊆ α выполняется (a • s)⁻¹ = a⁻¹ • s⁻¹.

LaTeX

$$$ (a\cdot s)^{-1} = a^{-1} \cdot s^{-1}. $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_op_smul_set_distrib (a : α) (s : Set α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹ := by ext;
  simp [mem_smul_set_iff_inv_smul_mem]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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