coe_le_coe — Mathlib

English

The order on fractional ideals is reflected by the order on their underlying submodules: (I : Submodule) ≤ (J : Submodule) iff I ≤ J.

Русский

Порядок дробных идеалов соответствует порядку их подмодулей: (I: Submodule) ≤ (J: Submodule) ⇔ I ≤ J.

LaTeX

$$$(I : \mathrm{Submodule} R P) \le (J : \mathrm{Submodule} R P) \iff I \le J$$$

Lean4

@[simp]
theorem coe_le_coe {I J : FractionalIdeal S P} : (I : Submodule R P) ≤ (J : Submodule R P) ↔ I ≤ J :=
  Iff.rfl

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