mathlib
935003eb - chore(data/nat/basic): add @[simp] to some lemmas about numerals (#6652)

Commit
4 years ago
chore(data/nat/basic): add @[simp] to some lemmas about numerals (#6652) Allows the simplifier to make more progress in equalities of numerals (both in nat, and in `[(semi)ring R] [no_zero_divisors R] [char_zero R]`). Also adds `@[simp]` to `nat.succ_ne_zero` and `nat.succ_ne_self`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Author
Parents
Loading