Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 03:36 e0f78ab3

View on Github →

chore(data/list/cycle): Add basic simp lemmas + minor golfing (#13533)

Estimated changes

Modified src/data/list/cycle.lean

added theorem cycle.card_to_multiset

modified def cycle.nil

modified theorem cycle.nil_to_multiset

added theorem cycle.to_finset_eq_nil

added theorem cycle.to_finset_to_multiset

added theorem cycle.to_multiset_eq_nil

Modified src/data/multiset/basic.lean

modified theorem multiset.coe_eq_zero