Commit 2022-11-26 15:48 f1d21e5d

View on Github →

chore: make argument to mul_inv_cancel implicit (#737) This matches mathlib3.

Estimated changes

added theorem mul_inv_cancel