Theorem mul_star_self_ne_zero

Modification history

2026-09-30 15:24
Mathlib/Algebra/Star/Basic.lean
feat(Algebra/Star/Basic): class for `star x * x = 0 → x = 0` (#44080) …
Added mul_star_self_ne_zeroView on Github →