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