dvd_symm — Mathlib

English

If p divides q and both are irreducible, then q divides p.

Русский

Если p делит q, и оба несводимы, тогда q делит p.

LaTeX

$$p \mid q \Rightarrow q \mid p$$

Lean4

/-- If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`. -/
theorem dvd_symm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) : p ∣ q → q ∣ p :=
  by
  rintro ⟨q', rfl⟩
  rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_isUnit)]

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