mul_right — Mathlib

English

Let m, n1, n2 be natural numbers with n1 ≠ 0 and n2 ≠ 0. Then qrSign(m, n1 n2) = qrSign(m, n1) · qrSign(m, n2).

Русский

Пусть m, n1, n2 ― натуральные числа, причём n1 ≠ 0 и n2 ≠ 0. Тогда qrSign(m, n1 n2) = qrSign(m, n1) · qrSign(m, n2).

LaTeX

$$$\forall m,n_1,n_2 \in \mathbb{N},\ n_1 \neq 0 \land n_2 \neq 0 \implies qrSign(m, n_1 n_2) = qrSign(m, n_1) \cdot qrSign(m, n_2)$$$

Lean4

/-- `qrSign` is multiplicative in the second argument. -/
theorem mul_right (m n₁ n₂ : ℕ) [NeZero n₁] [NeZero n₂] : qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂ :=
  jacobiSym.mul_right (χ₄ m) n₁ n₂

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