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

Commit ad0f42d

Browse files
jcommelinmergify[bot]
authored andcommitted
fix(data/nat/enat): Fix typo in lemma name (#1037)
1 parent c75c096 commit ad0f42d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/data/nat/enat.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ instance order_top : order_top enat :=
104104
lemma coe_lt_top (x : ℕ) : (x : enat) < ⊤ :=
105105
lt_of_le_of_ne le_top (λ h, absurd (congr_arg dom h) true_ne_false)
106106

107-
@[simp] lemma coe_ne_bot (x : ℕ) : (x : enat) ≠ ⊤ := ne_of_lt (coe_lt_top x)
107+
@[simp] lemma coe_ne_top (x : ℕ) : (x : enat) ≠ ⊤ := ne_of_lt (coe_lt_top x)
108108

109109
lemma pos_iff_one_le {x : enat} : 0 < x ↔ 1 ≤ x :=
110110
enat.cases_on x ⟨λ _, le_top, λ _, coe_lt_top _⟩

0 commit comments

Comments
 (0)