mul_left — Mathlib

English

qrSign is multiplicative in the first argument: qrSign(m1 * m2, n) = qrSign(m1, n) · qrSign(m2, n).

Русский

qrSign является мультипликативной по первому аргументу: qrSign(m1 · m2, n) = qrSign(m1, n) · qrSign(m2, n).

LaTeX

$$$ qrSign(m_1 \; m_2, n) = qrSign(m_1, n) \cdot qrSign(m_2, n) $$$

Lean4

/-- `qrSign` is multiplicative in the first argument. -/
theorem mul_left (m₁ m₂ n : ℕ) : qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n := by
  simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]

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