mul_le — Mathlib

English

For ideals I, J, K in a semiring R, I ⋅ J ⊆ K if and only if for every r ∈ I and s ∈ J, rs ∈ K.

Русский

Пусть I, J, K — идеалы полукольца R. Тогда I·J ⊆ K тогда и только тогда, когда для каждого r ∈ I и s ∈ J выполняется rs ∈ K.

LaTeX

$$$I \cdot J \le K \iff \forall r \in I,\ \forall s \in J,\ rs \in K$$$

Lean4

theorem mul_le : I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K :=
  Submodule.smul_le

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