Commit 2020-07-03 07:27 56ed551e

View on Github →

fix(algebra/group_with_zero): fix left/right (#3278) Rename mul_inv_cancel_left'/mul_inv_cancel_right' to match mul_inv_cancel_left/mul_inv_cancel_right.

Estimated changes

Modified src/algebra/group_with_zero.lean

modified theorem inv_mul_cancel_left'

modified theorem inv_mul_cancel_right'

modified theorem mul_inv_cancel_left'

modified theorem mul_inv_cancel_right'

Modified src/ring_theory/valuation/basic.lean