mathlib3
784fe06d - feat(analysis/calculus/deriv): generalize lemmas about deriv and `smul` (#10378)

Commit
4 years ago
feat(analysis/calculus/deriv): generalize lemmas about deriv and `smul` (#10378) Allow scalar multiplication by numbers from a different field.
Author
Parents
Loading