Commit 2023-10-21 19:10 3ce43c18

View on Github →

feat: Handle powers and multiplicative inverses in cancel_denoms (#7819) fixes #7732

Estimated changes

Modified Mathlib/Tactic/CancelDenoms/Core.lean

added theorem CancelDenoms.inv_subst

added theorem CancelDenoms.pow_subst

Modified test/cancel_denoms.lean

Modified test/linarith.lean