chore (Algebra.Basic): make RingHom.id and related declarations reducible #9025
Closed
mattrobball wants to merge 11 commits intomasterfrom mrb/reducible_algebra_id
+26-12
Commits
Commits on Dec 13, 2023
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
