Theorem SMul.smul_eq_hSMul

Modification history

2024-11-25 09:33
Mathlib/Algebra/Group/Defs.lean
chore: split notation typeclasses out of Algebra.Group.Defs (#19350)
Modified SMul.smul_eq_hSMulView on Github →
2023-12-15 19:04
Mathlib/Algebra/Group/Defs.lean
feat: port test/instance_diamonds.lean (#9037) …
Added SMul.smul_eq_hSMulView on Github →