Theorem isRegular_of_ne_zero'

Modification history

2026-01-21 17:08
Mathlib/Algebra/Ring/Regular.lean
chore(Algebra): rename `IsRegular_of_ne_zero` to `IsRegular.of_ne_zero` (#34206)
Deleted isRegular_of_ne_zero'View on Github →
2022-11-30 05:06
Mathlib/Algebra/Ring/Regular.lean
feat: port Algebra.Ring.Regular (#795) …
Added isRegular_of_ne_zero'View on Github →