mathlib

34b7361b - feat(algebra/*): Add ring instances to clifford_algebra and exterior_algebra (#4916)

feat(algebra/*): Add ring instances to clifford_algebra and exterior_algebra (#4916) To do this, this removes the `irreducible` attributes. These attributes were present to try and "insulate" the quotient / generator based definitions, and force downstream proofs to use the universal property. Unfortunately, this irreducibility created massive headaches in typeclass resolution, and the tradeoff for neatness vs usability just isn't worth it. If someone wants to add back the `irreducible` attributes in future, they now have test-cases that force them not to break the `ring` instances when doing so.