Theorem mul_mem_nonZeroDivisorsLeft_of_mem_nonZeroDivisorsLeft

Modification history

2026-08-11 12:14
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
chore: delete deprecated declarations/modules from January 2026 (#42075) …
Deleted mul_mem_nonZeroDivisorsLeft_of_mem_nonZeroDivisorsLeftView on Github →
2026-01-02 21:42
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication (#32773) …
Added mul_mem_nonZeroDivisorsLeft_of_mem_nonZeroDivisorsLeftView on Github →