Commit 2023-06-03 10:55 46443dc4

View on Github →

feat: port Algebra.Jordan.Basic (#4625)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Jordan/Basic.lean

added theorem commute_lmul_lmul_sq

added theorem commute_lmul_rmul

added theorem commute_lmul_rmul_sq

added theorem commute_lmul_sq_rmul

added theorem commute_rmul_rmul_sq

added theorem two_nsmul_lie_lmul_lmul_add_add_eq_zero

added theorem two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add