Commit 2025-07-24 08:42 29caf88d
View on Github →chore: split Data.Sign
(#27232)
We now have a Defs
file defining SignType
and basic instances, as well as a Basic
file proving results about the sign function on a ring.
The files have not been changed beyond updating the module description.