Commit 2023-11-16 23:07 79da87bb

View on Github →

fix: remove references to non-heterogenous operators in theorem statements (#8086) Some of these are likely porting errors. Statements should always be about the heterogenous versions because these are the ones with notation. For places where we are abusing defeq, this debuts the trick of using (by exact a : B) = (by exact a1) + (by exact b2) to ensure the = and + are typed as B instead of A.

Estimated changes

modified theorem CancelCommMonoid.ext
modified theorem CancelMonoid.ext
modified theorem CommMonoid.ext
modified theorem DivInvMonoid.ext
modified theorem LeftCancelMonoid.ext
modified theorem Monoid.ext
modified theorem RightCancelMonoid.ext