Theorem IsSMulRegular.zero

Modification history

2026-09-11 04:13

Mathlib/Algebra/GroupWithZero/Action/Regular.lean

chore(Algebra/Regular/SMul): split out GroupWithZero (#43679) …

Modified IsSMulRegular.zero View on Github →

2022-12-22 01:22

Mathlib/Algebra/Regular/SMul.lean

Feat: port algebra.regular.smul (#1154) …

Added IsSMulRegular.zero View on Github →