mathlib3
072cfc55 - chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801)

Commit

5 years ago

chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801) finsupp already has one, it seems pointless to hide the one for dfinsupp behind a def.

References

#4925 - Make prime-avoidance branch build

Author

eric-wieser

Parents

63c0dac6

mathlib3 072cfc55 - chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801)

mathlib3
072cfc55 - chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801)