Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-26 04:07 07d6d3f1

View on Github →

feat(algebra/algebra/basic): smul_mul_smul (#6423) An identity for algebras. (this PR is part of the irreducibility saga)

Estimated changes

added theorem algebra.smul_mul_smul