smul_mem_iff''

Mathlib.Algebra.Module.Submodule.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.smul_mem_iff''

← MathLib Explorer

English

If r is invertible, then r·x ∈ p ⇔ x ∈ p for all x ∈ M.

Русский

Если скаляр r обратим, то для любого x выполняется r·x ∈ p ⇔ x ∈ p.

LaTeX

$$$ [\\text{Invertible } r] \\Rightarrow (r·x \\in p \\iff x \\in p)$$$

Lean4

@[simp]
theorem smul_mem_iff'' [Invertible r] : r • x ∈ p ↔ x ∈ p :=
  by
  refine ⟨fun h ↦ ?_, p.smul_mem r⟩
  rw [← invOf_smul_smul r x]
  exact p.smul_mem _ h

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

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

Разделы

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

Аффилиация

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