coeSubmodule_le_coeSubmodule — Mathlib

English

For a fraction ring K of R with an algebra structure, the inequality between submodules is preserved: coeSubmodule K I ≤ coeSubmodule K J iff I ≤ J.

Русский

При наличии дробного кольца K над R неравенство подмодулов сохраняется: coeSubmodule K I ≤ coeSubmodule K J тогда и только тогда, когда I ≤ J.

LaTeX

$$coeSubmodule_le_coeSubmodule : (I ≤ J) ↔ (coeSubmodule K I ≤ coeSubmodule K J)$$

Lean4

@[simp, mono]
theorem coeSubmodule_le_coeSubmodule {I J : Ideal R} : coeSubmodule K I ≤ coeSubmodule K J ↔ I ≤ J :=
  IsLocalization.coeSubmodule_le_coeSubmodule le_rfl

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