Theorem CStarRing.star_mul_self_eq_zero_iff

Modification history

2026-09-30 15:24
Mathlib/Analysis/CStarAlgebra/Basic.lean
feat(Algebra/Star/Basic): class for `star x * x = 0 → x = 0` (#44080) …
Deleted CStarRing.star_mul_self_eq_zero_iffView on Github →
2024-08-06 04:16
Mathlib/Analysis/CStarAlgebra/Basic.lean
chore(*): rename `Cstar*` to `CStar*` (#15495) …
Added CStarRing.star_mul_self_eq_zero_iffView on Github →