Theorem mul_mem_nonZeroDivisors_of_mem_nonZeroDivisors

Modification history

2026-01-02 21:42

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication (#32773) …

Added mul_mem_nonZeroDivisors_of_mem_nonZeroDivisors View on Github →