le_div_iff_mul_le — Mathlib

English

Let I, J, K be submodules of a commutative algebra A over R. Then I is contained in the quotient J/K if and only if the product I·K is contained in J. Here J/K denotes the submodule consisting of all a ∈ A such that aK ⊆ J.

Русский

Пусть I, J, K — подмодули A над R. Тогда I ⊆ J/K тогда и только тогда I·K ⊆ J. Здесь J/K обозначает подмодуль, состоящий из элементов a ∈ A такие, что aK ⊆ J.

LaTeX

$$$I \le J / K \iff I K \le J$$$

Lean4

theorem le_div_iff_mul_le {I J K : Submodule R A} : I ≤ J / K ↔ I * K ≤ J := by rw [le_div_iff, mul_le]

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