mathlib3
dc4ad812 - refactor(*): lmul is an algebra hom (#4724)

Commit

5 years ago

refactor(*): lmul is an algebra hom (#4724) also, make some arguments implicit, and add simp lemmas

References

Author

jcommelin

Parents