NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

remark.  [ca-001C]
✍️source

    As ideals haven't been formalized for the non-commutative case, \(\textsf {Mathlib}\) uses RingQuot in places where the quotient of non-commutative rings by ideal is needed. The universal properties of the quotient are proven, and should be used instead of the definition that is subject to change.