Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.id.smul_eq_mul

Modification history

2019-11-13 12:44
src/ring_theory/algebra.lean
feat(analysis/calculus/deriv): one-dimensional derivatives (#1670) …
Added algebra.id.smul_eq_mulView on Github →