mathlib
5065471e - feat(data/monoid_algebra): add missing has_coe_to_fun (#4315)

Commit

5 years ago

feat(data/monoid_algebra): add missing has_coe_to_fun (#4315) Also does the same for the additive version `semimodule k (add_monoid_algebra k G)`.

References

Author

eric-wieser

Parents