English
The Legendre symbol defines a monoid-with-zero homomorphism from ℤ to ℤ, i.e., it preserves zero, one, and multiplication.
Русский
Символ Лежандра задаёт одомормфизм моноида с нулём из целых чисел в целые числа: сохраняет ноль, единицу и умножение.
LaTeX
$$$\mathrm{hom}: \mathbb{Z} \to_{\mathrm{MonoidWithZero}} \mathbb{Z},\quad \mathrm{toFun}=\mathrm{legendreSym}(p),\quad \mathrm{map\_zero'}=\mathrm{at\_zero}(p),\ \mathrm{map\_mul'}=\mathrm{legendreSym}.mul(p)$$$
Lean4
/-- The Legendre symbol is a homomorphism of monoids with zero. -/
@[simps]
def hom : ℤ →*₀ ℤ where
toFun := legendreSym p
map_zero' := at_zero p
map_one' := at_one p
map_mul' := legendreSym.mul p
