mathlib3
e1bccd6e - chore(data/int/order/basic): Fix lemma name (#17967)

Commit
2 years ago
chore(data/int/order/basic): Fix lemma name (#17967) `int.coe_nat_abs` wasn't referring to the correct lemma. Change the name, add the lemma it should correspond to and tag both with `simp` and `norm_cast`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading