Commit 2024-03-28 10:26 47a76467

View on Github →

refactor(Order/RelSeries): Use RelHom in RelSeries.map (#11730) split from #11147

Estimated changes

modified def RelSeries.map
modified theorem RelSeries.map_apply