Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tactic.ring.add_neg_eq_sub

Modification history

2020-12-11 13:45

src/tactic/ring.lean

chore(*): don't assume `sub_eq_add_neg` and `div_eq_mul_inv` are defeq (#5302) …

Modified tactic.ring.add_neg_eq_sub View on Github →

2018-09-10 03:23

tactic/ring.lean

feat(tactic/abel): decision procedure for comm groups

Modified tactic.ring.add_neg_eq_sub View on Github →

2018-01-14 01:53

tactic/ring.lean

feat(tactic/ring): use `ring` for rewriting into pretty print format

Added tactic.ring.add_neg_eq_sub View on Github →