Commit 2023-12-15 19:04 d58b5726

View on Github →

feat: port test/instance_diamonds.lean (#9037) This reveals that Smul.ext_iff is hard to work with unless we also have a lemma to convert SMul.smul to HSMul.hsMul

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

added theorem SMul.smul_eq_hSMul

Modified Mathlib/Data/Complex/Module.lean

Created test/instance_diamonds.lean

added theorem TensorProduct.f_apply