fderiv): use right actions instead of .smul_right for multiplication

Commit

3 years ago

refactor(analysis/calculus/fderiv): use right actions instead of .smul_right for multiplication The two are defeq, but the former is arguably easier to work with.

References

eric-wieser/less-smul_right

#17802 - refactor(analysis/calculus/fderiv): use right actions instead of .smul_right for multiplication

Author

eric-wieser

Parents

76658a41

mathlib 946dd921 - refactor(analysis/calculus/fderiv): use right actions instead of .smul_right for multiplication

mathlib
946dd921 - refactor(analysis/calculus/fderiv): use right actions instead of .smul_right for multiplication