inv_le_comm — Mathlib

English

For nonzero fractional ideals I and J, I^(-1) ≤ J if and only if J^(-1) ≤ I.

Русский

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

LaTeX

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

Lean4

theorem inv_le_comm {I J : FractionalIdeal A⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) : I⁻¹ ≤ J ↔ J⁻¹ ≤ I := by
  simpa using le_inv_comm (A := A) (K := K) (inv_ne_zero hI) (inv_ne_zero hJ)

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