feat(data/sym/basic): add nil coe lemma (#16181)

add simple coe lemma for sym.nil
leanprover-community · Aug 22, 2022 · 0705229 · 0705229
1 parent bfd2857
commit 0705229
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/data/sym/basic.lean b/src/data/sym/basic.lean
@@ -71,6 +71,8 @@ The unique element in `sym α 0`.
 -/
 @[pattern] def nil : sym α 0 := ⟨0, multiset.card_zero⟩
 
+@[simp] lemma coe_nil : (coe (@sym.nil α)) = (0 : multiset α) := rfl
+
 /--
 Inserts an element into the term of `sym α n`, increasing the length by one.
 -/