map_neg_divisorsAntidiag — Mathlib

English

The divisors antidiagonal is invariant under negating both coordinates, i.e., mapping (a, b) to (−a, −b) preserves membership in z.divisorsAntidiag.

Русский

Антидиагональ делителей инвариантна относительно отрицания обеих координат: если (a,b) в z.divisorsAntidiag, то (−a,−b) тоже в z.divisorsAntidiag.

LaTeX

$$$ (−a,−b) \in z.divisorsAntidiag \iff (a,b) \in z.divisorsAntidiag $$$

Lean4

@[simp]
theorem map_neg_divisorsAntidiag : z.divisorsAntidiag.map (Equiv.neg _).toEmbedding = z.divisorsAntidiag := by ext;
  simp [mem_divisorsAntidiag, mul_comm]

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