dvdNotUnit_iff_lt — Mathlib

English

For ideals I and J in a Dedekind domain, I divides J with a nonunit quotient if and only if J is strictly contained in I.

Русский

Для идеалов I и J в детерминантном домене, существование делимости I на J с ненулевым несобственным делителем эквивалентно строгому включению J в I.

LaTeX

$$$DvdNotUnit(I,J) \iff J < I$$$

Lean4

theorem dvdNotUnit_iff_lt {I J : Ideal A} : DvdNotUnit I J ↔ J < I :=
  ⟨fun ⟨hI, H, hunit, hmul⟩ =>
    lt_of_le_of_ne (Ideal.dvd_iff_le.mp ⟨H, hmul⟩)
      (mt
        (fun h =>
          have : H = 1 := mul_left_cancel₀ hI (by rw [← hmul, h, mul_one])
          show IsUnit H from this.symm ▸ isUnit_one)
        hunit),
    fun h => dvdNotUnit_of_dvd_of_not_dvd (Ideal.dvd_iff_le.mpr (le_of_lt h)) (mt Ideal.dvd_iff_le.mp (not_le_of_gt h))⟩

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