Commit 2025-09-01 12:03 8acd6dfb
View on Github →chore(RingTheory): process porting notes, part 1 (#29112) This PR goes through all the porting notes in the RingTheory subfolders up to Kaehler and fixes the ones that have an obvious solution. Quite a few of these were fixed already but the note was never removed!