Commit 2024-06-16 11:38 0c9132ba
View on Github →feat: a ^ (p - 1) = if a ≠ 0 then 1 else 0
in ZMod p
(#13828)
This is useful for algebraically encoding equality of indices.
From LeanCamCombi
feat: a ^ (p - 1) = if a ≠ 0 then 1 else 0
in ZMod p
(#13828)
This is useful for algebraically encoding equality of indices.
From LeanCamCombi