neg_iff — Mathlib

English

Let a,b be elements of a ring α. The finiteness property described by FiniteMultiplicity is unaffected when b is replaced by its additive inverse; i.e., FiniteMultiplicity a (−b) holds if and only if FiniteMultiplicity a b holds.

Русский

Пусть a,b — элементы кольца α. Свойство конечной кратности относительно −b эквивалентно свойству относительно b: FiniteMultiplicity a (−b) эквивалентно FiniteMultiplicity a b.

LaTeX

$$$\\operatorname{FiniteMultiplicity}(a,-b) \\leftrightarrow \\operatorname{FiniteMultiplicity}(a,b)$$$

Lean4

@[simp]
theorem neg_iff {a b : α} : FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b :=
  by
  unfold FiniteMultiplicity
  congr! 3
  simp only [dvd_neg]

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