TwoSidedIdeal

Stream: FLT

[Ruben Van de Velde]

Do we want to replace RingCon by the new TwoSidedIdeal from #13902?

[Kevin Buzzard]

No, students have taken over the development of central simple algebras in their own repo. Similarly Amelia is developing coalgebras/Hopf algebras and PRing directly to mathlib, and I'm moving Frobenius elements to mathlib; right now most of my FLT time comprising getting stuff out of FLT.