Commit 2025-08-18 09:17 7679b3b2
View on Github →chore(Algebra): more porting notes for Algebra (#28409) I went through all porting notes for the Algebra folders between Group and Order. A lot of them are fixed now, some we won't fix (such as Lean 4 being stricter about type synonyms). Either way, we can get rid of a lot of them.