Theorem mul_mul_mul_comm'

Modification history

2025-11-01 12:56
Mathlib/Algebra/Group/Basic.lean
feat(Mathlib/Algebra/QuadraticAlgebra): norm, star structure on quadratic alg. (#30059) …
Added mul_mul_mul_comm'View on Github →