Mathlib Changelog
v4
Changelog
About
Github
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