le_div_iff_mul_le — Mathlib

English

Let I, J, J' be fractional ideals with J' ≠ 0. Then I ≤ J / J' if and only if I ⋅ J' ≤ J.

Русский

Пусть I, J, J' — дробные идеалы, и J' не равен нулю. Тогда I ≤ J / J' тогда и только тогда I ⋅ J' ≤ J.

LaTeX

$$$ (J' \neq 0) \Rightarrow \bigl( I \le J / J' \iff I \cdot J' \le J \bigr) $$$

Lean4

theorem le_div_iff_mul_le {I J J' : FractionalIdeal R₁⁰ K} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ I * J' ≤ J :=
  by
  rw [div_nonzero hJ', ← coe_le_coe (I := I * J') (J := J), coe_mul]
  exact Submodule.le_div_iff_mul_le

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