eq_iff_eq — Mathlib

English

For odd m and odd n and integers x,y, we have qrSign(m, n)·x = y if and only if x = qrSign(m, n)·y.

Русский

Для нечётных m и n и целых x,y верно qrSign(m, n)·x = y тогда и только тогда, когда x = qrSign(m, n)·y.

LaTeX

$$$\forall m,n \; (\text{Odd}(m) \land \text{Odd}(n)) \; \forall x,y \in \mathbb{Z},\ qrSign(m,n) \cdot x = y \iff x = qrSign(m,n) \cdot y$$$

Lean4

/-- We can move `qrSign m n` from one side of an equality to the other when `m` and `n` are odd. -/
theorem eq_iff_eq {m n : ℕ} (hm : Odd m) (hn : Odd n) (x y : ℤ) : qrSign m n * x = y ↔ x = qrSign m n * y := by
  refine
      ⟨fun h' =>
        let h := h'.symm
        ?_,
        fun h => ?_⟩ <;>
    rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]

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