le_inv_comm — Mathlib

English

For nonzero fractional ideals I and J in a Dedekind domain A with fraction field K, I ≤ J^(-1) if and only if J ≤ I^(-1).

Русский

Для непустых дробных идеалов I и J в области Дедекина A с полем частиц K выполняется: I ≤ J^{-1} тогда и только если J ≤ I^{-1}.

LaTeX

$$$I \\le J^{-1} \\iff J \\le I^{-1}$$$

Lean4

theorem le_inv_comm {I J : FractionalIdeal A⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) : I ≤ J⁻¹ ↔ J ≤ I⁻¹ := by
  rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]

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