Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-31 00:41 6f6ee003

View on Github →

chore(data/finsupp): add simp lemmas about dom_congr (#6963) Inspired by #6905

Estimated changes

added theorem finsupp.dom_congr_refl
added theorem finsupp.dom_congr_symm