mem_invOf_smul_set

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

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

English

If a is invertible, then b belongs to the inverse-scalar translate ⅟a • s if and only if a • b belongs to s.

Русский

Если a обратим, то b ∈ ⅟a • s тогда и только тогда, когда a • b ∈ s.

LaTeX

$$$[Invertible\\ a]\\ b \\in ⅟a \\cdot s \\iff a \\cdot b \\in s$$$

Lean4

@[simp]
theorem mem_invOf_smul_set [Invertible a] : b ∈ ⅟a • s ↔ a • b ∈ s :=
  mem_inv_smul_set_iff (a := unitOfInvertible a)

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

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

Разделы

Аффилиация

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