Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit b44fa3c

Browse files
committed
chore(data/int/basic): mark cast_sub with simp attribute (#2687)
I think the reason this didn't have the `simp` attribute already was from the time when `sub_eq_add_neg` was a `simp` lemma, so it wasn't necessary. I'm adding the `simp` attribute back now that `sub_eq_add_neg` is not a `simp` lemma.
1 parent f07ac36 commit b44fa3c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/data/int/basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1164,7 +1164,7 @@ end
11641164
| (n : ℕ) := cast_neg_of_nat _
11651165
| -[1+ n] := (neg_neg _).symm
11661166

1167-
@[norm_cast] theorem cast_sub [add_group α] [has_one α] (m n) : ((m - n : ℤ) : α) = m - n :=
1167+
@[simp, norm_cast] theorem cast_sub [add_group α] [has_one α] (m n) : ((m - n : ℤ) : α) = m - n :=
11681168
by simp [sub_eq_add_neg]
11691169

11701170
@[simp] theorem cast_eq_zero [add_group α] [has_one α] [char_zero α] {n : ℤ} : (n : α) = 0 ↔ n = 0 :=

0 commit comments

Comments
 (0)