Commit 2021-04-22 14:56 918aea72
View on Github →refactor(algebra/ring_quot.lean): make ring_quot irreducible (#7120)
The quotient of a ring by an equivalence relation which is compatible with the operations is still a ring. This is used to define several objects such as tensor algebras, exterior algebras, and so on, but the details of the construction are irrelevant. This PR makes ring_quot irreducible to keep the complexity down.