dvd_iff — Mathlib

English

For Monoid M, if x is irreducible, then y | x iff either y is a unit or y is associated to x.

Русский

Для моноида M, если x ирредуцируемо, то y делит x тогда и только тогда, когда y единица или y ассоциировано с x.

LaTeX

$$$ [Monoid M] {x y : M} (hx : Irreducible x) : (\exists z, x = z * ? ) \Rightarrow \dots$$$

Lean4

theorem dvd_iff [Monoid M] {x y : M} (hx : Irreducible x) : y ∣ x ↔ IsUnit y ∨ Associated x y :=
  by
  constructor
  · rintro ⟨z, hz⟩
    obtain (h | h) := hx.isUnit_or_isUnit hz
    · exact Or.inl h
    · rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)
  · rintro (hy | h)
    · exact hy.dvd
    · exact h.symm.dvd

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