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!

Estimated changes