Commit 2026-01-02 21:42 3135fb23

View on Github →

feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication (#32773) Similar to Is{Left,Right,}Regular.mul.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

added theorem mem_nonZeroDivisors_iff'

added theorem mul_mem_nonZeroDivisorsLeft_of_mem_nonZeroDivisorsLeft

added theorem mul_mem_nonZeroDivisorsRight_of_mem_nonZeroDivisorsRight

added theorem mul_mem_nonZeroDivisors_of_mem_nonZeroDivisors