Commit 2024-08-30 15:20 405a9bdd

View on Github →

feat: (a • b) * c • d = (a * c) • (b * d) (#16245) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Group/Action/Defs.lean

added theorem mul_smul_mul_comm

deleted theorem smul_mul_smul

added theorem smul_mul_smul_comm

Modified Mathlib/Algebra/Group/Action/Prod.lean

Modified Mathlib/Algebra/Group/Action/Units.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Algebra/SMulWithZero.lean

Modified Mathlib/Algebra/Star/Order.lean

Modified Mathlib/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

Modified Mathlib/RingTheory/LittleWedderburn.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean