Commit 2023-07-24 09:11 95a48b51

View on Github →

feat: add scalar tower instances for RingQuot and BilinForm (#6066) I tidied up some universe and type variables in the RingQuot file while I was here (in the first commit).

Estimated changes

modified theorem RingQuot.Rel.neg
modified theorem RingQuot.Rel.sub_left
modified theorem RingQuot.Rel.sub_right
modified theorem RingQuot.neg_quot
modified theorem RingQuot.ringQuot_ext
modified def RingQuot.starRing
modified theorem RingQuot.sub_quot