mathlib
94e9bb55 - chore(data/{finsupp,dfinsupp}/basic): use the injective APIs (#12534)

Commit
3 years ago
chore(data/{finsupp,dfinsupp}/basic): use the injective APIs (#12534) This also fixes a scalar diamond in the `nat` and `int` actions on `dfinsupp`. The diamond did not exist for `finsupp`.
Author
Parents
Loading