pointwise_smul_le_iff₀ — Mathlib

English

For a ≠ 0 in GroupWithZero M acting on R, S ≤ a • T iff a^{-1} • S ≤ T for Subsemirings S,T.

Русский

Для a ≠ 0 в GroupWithZero M действии на Subsemiring R выполняется S ≤ a • T ⇔ a^{-1} • S ≤ T.

LaTeX

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

Lean4

theorem pointwise_smul_le_iff₀ {a : M} (ha : a ≠ 0) {S T : Subsemiring R} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
  smul_set_subset_iff₀ ha

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