Theorem mul_star_self_pos_iff

Modification history

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