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

Estimated changes