le_pointwise_smul_iff₀

Mathlib.Algebra.Ring.Subring.Pointwise

URI: https://scilib.ai/kg/mathlib#Subring.le_pointwise_smul_iff₀

English

For a nonzero a and subrings S, T, S ≤ a · T iff a^{-1} · S ≤ T.

Русский

Для ненулевого a и подкольц S, T: S ≤ a · T эквивалентно a^{-1} · S ≤ T.

LaTeX

$$$a \neq 0 \Rightarrow (S \le a \cdot T \iff a^{-1} \cdot S \le T)$$$

Lean4

theorem le_pointwise_smul_iff₀ {a : M} (ha : a ≠ 0) {S T : Subring R} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
  subset_smul_set_iff₀ ha

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

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

Разделы

Аффилиация

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