dvdNotUnit_of_dvdNotUnit_associated

English

Transitivity of DvdNotUnit under association: if p divides q nontrivially and q is associated to r, then p divides r nontrivially.

Русский

Транзитивность DvdNotUnit при ассоциации: если p делится q не единицей и q ассоциируется с r, то p делится на r не единицей.

LaTeX

$$$ DvdNotUnit p q \to Associated q r \to DvdNotUnit p r $$$

Lean4

theorem dvdNotUnit_of_dvdNotUnit_associated [CommMonoidWithZero M] [Nontrivial M] {p q r : M} (h : DvdNotUnit p q)
    (h' : Associated q r) : DvdNotUnit p r :=
  by
  obtain ⟨u, rfl⟩ := Associated.symm h'
  obtain ⟨hp, x, hx⟩ := h
  refine ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, ?_⟩
  rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]

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