subset_pointwise_smul_iff — Mathlib

English

For any a ∈ M and ideals S,T of R, S ≤ a • T if and only if a^{-1} • S ≤ T.

Русский

Для любого a ∈ M и идеалов S,T в R верно S ≤ a • T тогда и только тогда a^{-1} • S ≤ T.

LaTeX

$$$\forall a \in M\, \forall S,T \in \text{Ideal}(R):\ S \le a \cdot T \iff a^{-1} \cdot S \le T$$$

Lean4

theorem subset_pointwise_smul_iff {a : M} {S T : Ideal R} : S ≤ a • T ↔ a⁻¹ • S ≤ T := by
  rw [← pointwise_smul_le_pointwise_smul_iff (a := a⁻¹), inv_smul_smul]

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