Skip to content

Commit

Permalink
chore: remove unused @[simp] from Fin.sub_one_lt_iff (#11967)
Browse files Browse the repository at this point in the history
The @[simp] annotation is not used in mathlib, and triggered a linter failure that I don't care to investigate unnecessarily.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Apr 16, 2024
1 parent d40db77 commit 73db0f6
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Mathlib/Data/Fin/Basic.lean
Expand Up @@ -1609,7 +1609,6 @@ theorem le_sub_one_iff {n : ℕ} {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 := by
simp
#align fin.le_sub_one_iff Fin.le_sub_one_iff

@[simp]
theorem sub_one_lt_iff {n : ℕ} {k : Fin (n + 1)} : k - 1 < k ↔ 0 < k :=
not_iff_not.1 <| by simp only [not_lt, le_sub_one_iff, le_zero_iff]
#align fin.sub_one_lt_iff Fin.sub_one_lt_iff
Expand Down

0 comments on commit 73db0f6

Please sign in to comment.