Commit 2023-05-10 11:33 a07d7509
View on Github →refactor(algebra): Redefine a ≡ b [PMOD p] (#18958)
as ∃ n : ℤ, b - a = n • p instead of ∀ n : ℤ, b - n • p ∉ set.Ioo a (a + p). Since this new definition doesn't require an order on α, we move it to a new file algebra.modeq. Expand the API.