Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 11:25 320ea398

View on Github →

feat(data/dfinsupp/basic): add missing lemmas about single (#14815) These lemmas were missed in #13076:

  • comap_domain_single
  • comap_domain'_single
  • sigma_curry_single
  • sigma_uncurry_single
  • extend_with_single_zero
  • extend_with_zero These are useful since many induction principles replace a generic dfinsupp with dfinsupp.single.

Estimated changes