Theorem SMul.smul_eq_hSMul

Modification history

2025-10-23 19:05
Mathlib/Algebra/Notation/Defs.lean
chore: revert #30788 and #30785 (#30807)
Deleted SMul.smul_eq_hSMulView on Github →
2025-10-22 14:25
Mathlib/Algebra/Notation/Defs.lean
chore: revert #30740 and #30748 (#30788) …
Added SMul.smul_eq_hSMulView on Github →
2025-10-21 18:15
Mathlib/Algebra/Notation/Defs.lean
chore: merge bump/v4.25.0 (#30740)
Deleted SMul.smul_eq_hSMulView on Github →
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 →