Theorem ite_zero_smul

Modification history

2025-03-05 10:07

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

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

Modified ite_zero_smul View on Github →

2023-12-04 15:55

Mathlib/Algebra/SMulWithZero.lean

feat: `(if P then 1 else 0) • a` (#8347) …

Added ite_zero_smul View on Github →