pointwise_smul_subset_iff

Mathlib.Algebra.Ring.Subring.Pointwise

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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