dvd_neg — Mathlib

English

In a semigroup with distributive negation, a ∣ -b ↔ a ∣ b.

Русский

В полугруппе с распределительным отрицанием a | −b ⇔ a | b.

LaTeX

$$$a \mid -b \iff a \mid b$$$

Lean4

/-- An element `a` of a semigroup with a distributive negation divides the negation of an element
`b` iff `a` divides `b`. -/
@[simp]
theorem dvd_neg : a ∣ -b ↔ a ∣ b :=
  (Equiv.neg _).exists_congr_left.trans <| by simp only [Equiv.neg_symm, Equiv.neg_apply, mul_neg, neg_inj, Dvd.dvd]

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