English
If a divides b and b divides a in a CancelMonoidWithZero, then a is associated with b.
Русский
Если a делит b и b делит a в CancelMonoidWithZero, то a ассоциировано с b.
LaTeX
$$$ [CancelMonoidWithZero M] {a b : M} (hab : a \mid b) (hba : b \mid a) : a ~ᵤ b $$$
Lean4
theorem associated_of_dvd_dvd [CancelMonoidWithZero M] {a b : M} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
by
rcases hab with ⟨c, rfl⟩
rcases hba with ⟨d, a_eq⟩
by_cases ha0 : a = 0
· simp_all
have hac0 : a * c ≠ 0 := by
intro con
rw [con, zero_mul] at a_eq
apply ha0 a_eq
have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
