Commit 2025-08-08 08:35 cf0b42e1

fix: restore the algebraic instances on UInt types (#27540) These were deleted without comment in the 4.20.0 upgrade (https://github.com/leanprover-community/mathlib4/commit/7d6781bab0100467855789de1053ccabeed34520), presumably because they were annoying to fix. This follows the advice in the comment to make a PR to restore them. These should be much less fragile than before, as rfl is no longer used for any of the proofs about data defined elsewhere. Some fragile theorems remain, but they can be upstreamed and then deleted. #lean4 > open scoped UInt64.CommRing @ 💬