le_pointwise_smul_iff₀

Mathlib.Algebra.GroupWithZero.Subgroup

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

English

For ha ≠ 0, S ≤ a • T ↔ a⁻¹ • S ≤ T.

Русский

Пусть ha ≠ 0. Тогда S ≤ a • T ⇔ a⁻¹ • S ≤ T.

LaTeX

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

Lean4

theorem le_pointwise_smul_iff₀ (ha : a ≠ 0) : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
  subset_smul_set_iff₀ ha

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

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

Разделы

Аффилиация

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