Theorem smul_mul_smul_comm

Modification history

2024-08-30 15:20
Mathlib/Algebra/Group/Action/Defs.lean
feat: `(a • b) * c • d = (a * c) • (b * d)` (#16245) …
Added smul_mul_smul_commView on Github →