Theorem zero_smul

Modification history

2025-03-05 10:07

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

chore: move `SMulWithZero` with `SMulZeroClass` (#13027) …

Modified zero_smul View on Github →

2022-12-21 05:43

Mathlib/Algebra/SmulWithZero.lean

feat: port Algebra.SmulWithZero (#1130)

Added zero_smul View on Github →