pointwise_smul_le_pointwise_smul_iff₀

Mathlib.Algebra.Ring.Subring.Pointwise

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

← MathLib Explorer

English

If a ≠ 0 and S, T are Subrings, then a · S ≤ a · T implies S ≤ T.

Русский

Если a ≠ 0 и S, T — подкольца, то a · S ≤ a · T влечёт S ≤ T.

LaTeX

$$$a \neq 0 \Rightarrow (a \cdot S \le a \cdot T \Rightarrow S \le T)$$$

Lean4

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff₀ {a : M} (ha : a ≠ 0) {S T : Subring R} : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff₀ ha

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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