basic): add `can_lift (α → M₀) (α →₀ M₀)` (#6777)

Commit

4 years ago

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

Author

urkud

Parents