English
A commutative Jordan multiplication is also a Jordan multiplication.
Русский
Коммутативное умножение с выполняемым условием Джордана образует также структуру Джорданова умножения.
LaTeX
$$[CommMagma A] [IsCommJordan A] \Rightarrow IsJordan A$$
Lean4
/-- A (commutative) Jordan multiplication is also a Jordan multiplication -/
instance (priority := 100) toIsJordan [CommMagma A] [IsCommJordan A] : IsJordan A
where
lmul_comm_rmul a b := by rw [mul_comm, mul_comm a b]
lmul_lmul_comm_lmul a b := by rw [mul_comm (a * a) (a * b), IsCommJordan.lmul_comm_rmul_rmul, mul_comm b (a * a)]
lmul_comm_rmul_rmul := IsCommJordan.lmul_comm_rmul_rmul
lmul_lmul_comm_rmul a
b := by rw [mul_comm (a * a) (b * a), mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, mul_comm, mul_comm b (a * a)]
rmul_comm_rmul_rmul a
b := by
rw [mul_comm b a, IsCommJordan.lmul_comm_rmul_rmul, mul_comm]
-- see Note [lower instance priority]
