Commit 2024-11-27 09:56 13419097
View on Github →feat: prove zmodRepr is unique (#19391)
We prove PadicInt.exists_unique_mem_range which is a strengthening of exists_mem_range, proving uniqueness of the natural number. I need this to simplify toZMod(1+ap) to 1.