neg_dvd — Mathlib

English

The negation of an element divides another element iff the element divides the other.

Русский

Отрицание элемента делит другое тогда и только тогда, когда сам элемент делит другое.

LaTeX

$$$\forall a b, \ semigroupDvd.dvd (-a) b \iff \ semigroupDvd.dvd a b$$$

Lean4

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

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