mem_smul_pointwise_iff_exists

Mathlib.Algebra.Ring.Subring.Pointwise

URI: https://scilib.ai/kg/mathlib#Subring.mem_smul_pointwise_iff_exists

← MathLib Explorer

English

A subring of a strictly ordered ring is a strictly ordered ring.

Русский

Подкольцо строго упорядоченного кольца является строго упорядоченным кольцом.

LaTeX

$$$IsStrictOrderedRing\; (\text{Subring } R)$$$

Lean4

theorem mem_smul_pointwise_iff_exists (m : M) (r : R) (S : Subring R) : r ∈ m • S ↔ ∃ s : R, s ∈ S ∧ m • s = r :=
  (Set.mem_smul_set : r ∈ m • (S : Set R) ↔ _)

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

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

Разделы

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

Аффилиация

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