Commit 2026-03-05 21:52 d0f4c1bb
View on Github →chore: fix typo (#35993)
There is a typo in this lemma.
I think it would be nice to add this to simp (and remove symm_toRingEquiv from the simp set) but it breaks downwards proofs which are annoying to fix since Ideal.map has not been refactored yet.