Theorem mul_smul_mul_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 mul_smul_mul_commView on Github →