spanSingleton_le_iff_mem

Mathlib.RingTheory.FractionalIdeal.Operations

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.spanSingleton_le_iff_mem

← MathLib Explorer

English

spanSingleton S x ≤ I if and only if x ∈ I.

Русский

spanSingleton S x ≤ I тогда и только тогда, когда x ∈ I.

LaTeX

$$$ \operatorname{spanSingleton} S x \le I \iff x \in I $$$

Lean4

@[simp]
theorem spanSingleton_le_iff_mem {x : P} {I : FractionalIdeal S P} : spanSingleton S x ≤ I ↔ x ∈ I := by
  rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]

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

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

Разделы

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

Аффилиация

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