subset_pointwise_smul_iff

Mathlib.Algebra.Ring.Subsemiring.Pointwise

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

English

For a ≠ 0, S ≤ a•T iff a⁻¹•S ≤ T (subset version).

Русский

При a ≠ 0: S ≤ a•T эквивалентно a⁻¹•S ≤ T (версия для подмножеств).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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