Commit 2024-05-11 08:45 01f894dc
View on Github →chore: split RingTheory.Ideal.Operations
(#12777)
Split the file RingTheory.Ideal.Operations
into two parts by putting everything related to maps into a new file called... RingTheory.Ideal.Maps
.