data/multiset/range): add multiset.coe_range (#15201)

leanprover-community · Jul 11, 2022 · aae01cd · aae01cd
1 parent 627bd0c
commit aae01cd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/data/multiset/range.lean b/src/data/multiset/range.lean
@@ -18,6 +18,8 @@ namespace multiset
   that is, the set `{0, 1, ..., n-1}`. -/
 def range (n : ℕ) : multiset ℕ := range n
 
+theorem coe_range (n : ℕ) : ↑(list.range n) = range n := rfl
+
 @[simp] theorem range_zero : range 0 = 0 := rfl
 
 @[simp] theorem range_succ (n : ℕ) : range (succ n) = n ::ₘ range n :=