Commit 2023-12-04 11:39 afa20325

View on Github →

chore: move Associates.quot_out earlier (#8484) And don't require commutativity while we're here.

Estimated changes

added theorem Associates.quot_out
deleted theorem Associates.quot_out