Commit 2025-03-28 16:45 718d4fea

View on Github →

chore(RingTheory): even more erws (#23404) Nothing very exciting, just a few manual unfolds and a few erws removed through proof refactoring.

Estimated changes