subset_pointwise_smul_iff

Mathlib.Algebra.Ring.Subring.Pointwise

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

English

For a ∈ M and subrings S, T of R, S ⊆ a · T if and only if a^{-1} · S ⊆ T.

Русский

Для a ∈ M и подкольц S, T верно: S ⊆ a · T тогда и только если a^{-1} · S ⊆ T.

LaTeX

$$$S \subseteq a \cdot T \iff a^{-1} \cdot S \subseteq T$$$

Lean4

theorem subset_pointwise_smul_iff {a : M} {S T : Subring R} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
  subset_smul_set_iff

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

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

Разделы

Аффилиация

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