Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-22 16:18 e54f6339

View on Github →

feat(data/finsupp/basic): add can_lift (α → M₀) (α →₀ M₀) (#6777) Also add a few missing simp/norm_cast lemmas.

Estimated changes

modified theorem finset.coe_empty
added theorem finset.coe_eq_empty
added theorem finsupp.coe_eq_zero
added theorem finsupp.coe_fn_inj
modified theorem finsupp.coe_zero
deleted theorem finsupp.finite_supp
added theorem finsupp.finite_support
modified theorem finsupp.fun_support_eq