mul_le — Mathlib

English

The product I·J is contained in K if and only if every product i·j with i ∈ I and j ∈ J lies in K.

Русский

Произведение I·J содержится в K тогда, когда каждый элемент i ∈ I и j ∈ J удовлетворяет i j ∈ K.

LaTeX

$$$I J \le K \;\Leftrightarrow\; \forall i\in I, \forall j\in J, i j \in K$$$

Lean4

theorem mul_le {I J K : FractionalIdeal S P} : I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K :=
  by
  simp only [mul_def]
  exact Submodule.mul_le

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