dvd_dvd_iff_associated — Mathlib

English

In a CancelMonoidWithZero, a divides b and b divides a iff a is associated with b.

Русский

В CancelMonoidWithZero: a делит b и b делит a тогда и только тогда, когда a ассоциировано с b.

LaTeX

$$$ [CancelMonoidWithZero M] {a b : M} : a \mid b \land b \mid a \iff a ~ᵤ b $$$

Lean4

theorem dvd_dvd_iff_associated [CancelMonoidWithZero M] {a b : M} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
  ⟨fun ⟨h1, h2⟩ => associated_of_dvd_dvd h1 h2, Associated.dvd_dvd⟩

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