Commit 2025-02-25 18:02 babf9a89
View on Github →chore(AlgebraicGeometry): clean up erw and porting notes (#22272)
I searched for erw and porting note and did my best to fix them. One recurring issue is that ext got less powerful than in Lean 3, the best solution is probably to make more @[ext] lemmas. But that would require more thought about library design than I have available right now.