mul_right — Mathlib

English

Jacobi symbol is multiplicative in its second argument: J(a|b1*b2) = J(a|b1) J(a|b2) when b1,b2 > 0.

Русский

Символ Якоби умножается по второму аргументу: J(a|b1 b2) = J(a|b1) J(a|b2), если b1,b2 > 0.

LaTeX

$$$J(a|b_1 b_2) = J(a|b_1) \cdot J(a|b_2)$$$

Lean4

/-- The Jacobi symbol is multiplicative in its second argument. -/
theorem mul_right (a : ℤ) (b₁ b₂ : ℕ) [NeZero b₁] [NeZero b₂] : J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂) :=
  mul_right' a (NeZero.ne b₁) (NeZero.ne b₂)

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