Commit 2025-10-03 15:29 17b380cd

View on Github →

chore(Algebra/Ring/Invertible): fix two names (#30166)

Estimated changes

added theorem AddUnits.neg_mulLeft
added theorem AddUnits.neg_mulRight
deleted theorem AddUnits.neg_mul_left
deleted theorem AddUnits.neg_mul_right