Diff — Multiplication

Revision #1418 → #1757 · back to history

addedImaginary unit squared6f8fe01f9b37

modifiedOrder preserved by positive factor84041eb3b635

Field	From #1418	To #1757
mathlib.module	Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs	Mathlib.Algebra.Order.GroupWithZero.Defs

modifiedNoncommutativity for matrices and quaternions797ea06ead5e

Field	From #1418	To #1757
mathlib.decl	Matrix.instMul	Matrix.instMulOfFintypeOfAddCommMonoid