Theorem isRegular_of_ne_zero

Modification history

2026-01-21 17:08
Mathlib/Algebra/GroupWithZero/Regular.lean
chore(Algebra): rename `IsRegular_of_ne_zero` to `IsRegular.of_ne_zero` (#34206)
Deleted isRegular_of_ne_zeroView on Github →
2025-06-24 10:56
Mathlib/Algebra/GroupWithZero/Regular.lean
refactor: move the definition of `IsRegular` earlier (#26321) …
Modified isRegular_of_ne_zeroView on Github →
2022-11-28 16:05
Mathlib/Algebra/Regular/Basic.lean
feat(Algebra/Regular/Basic): port file (#758) …
Added isRegular_of_ne_zeroView on Github →