Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-21 17:25 7073c8b9

View on Github →

feat(tactic/cancel_denoms): try to remove numeral denominators (#3109)

Estimated changes

Created src/tactic/cancel_denoms.lean

added theorem cancel_factors.add_subst

added theorem cancel_factors.cancel_factors_eq

added theorem cancel_factors.cancel_factors_eq_div

added theorem cancel_factors.cancel_factors_le

added theorem cancel_factors.cancel_factors_lt

added theorem cancel_factors.div_subst

added theorem cancel_factors.mul_subst

added theorem cancel_factors.neg_subst

added theorem cancel_factors.sub_subst

Modified src/tactic/default.lean

Modified src/tactic/interactive.lean

Created test/cancel_denoms.lean