Mathlib v3 is deprecated. Go to Mathlib v4

Theorem not_is_regular_zero

Modification history

2021-03-15 09:03

src/algebra/regular.lean

feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introduce `mul_action_with_zero` and `M`-regular elements (#6590) …

Added not_is_regular_zero View on Github →