mathlib
bfa6bbbc - doc(algebra/algebra/basic): add a comment to make the similar definition discoverable (#8500)

Commit
4 years ago
doc(algebra/algebra/basic): add a comment to make the similar definition discoverable (#8500) I couldn't find this def, but was able to find lmul.
Author
Parents
Loading