mul — Mathlib

English

For fixed p, the Legendre symbol is multiplicative in a: legendreSym p (a b) = legendreSym p a · legendreSym p b.

Русский

При фиксированном p знак Лежандра по переменной a умножается: legendreSym p (a b) = legendreSym p a · legendreSym p b.

LaTeX

$$$\mathrm{legendreSym}(p,ab) = \mathrm{legendreSym}(p,a) \cdot \mathrm{legendreSym}(p,b)$$$

Lean4

/-- The Legendre symbol is multiplicative in `a` for `p` fixed. -/
protected theorem mul (a b : ℤ) : legendreSym p (a * b) = legendreSym p a * legendreSym p b := by
  simp [legendreSym, Int.cast_mul, map_mul]

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