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)
Added IsRegular.of_ne_zeroView on Github →