mathlib
90d2046b - feat(algebra/monoid_algebra): adjointness for the functor `G ↦ monoid_algebra k G` when `G` carries only `has_mul` (#7932)

Commit

4 years ago

feat(algebra/monoid_algebra): adjointness for the functor `G ↦ monoid_algebra k G` when `G` carries only `has_mul` (#7932) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

ocfnash

Parents

d521b2bc

mathlib 90d2046b - feat(algebra/monoid_algebra): adjointness for the functor `G ↦ monoid_algebra k G` when `G` carries only `has_mul` (#7932)

mathlib
90d2046b - feat(algebra/monoid_algebra): adjointness for the functor `G ↦ monoid_algebra k G` when `G` carries only `has_mul` (#7932)