Commit 2026-09-30 15:24 b0217dff

View on Github →

feat(Algebra/Star/Basic): class for star x * x = 0 → x = 0 (#44080) A star ring has IsProperStar when star x * x = 0 implies x = 0. For a star ring with no zero divisors, this is automatic. But this is also true for CStarRings, matrices, etc. So this is meant to weaken the NoZeroDivisors hypothesis when we only need star x * x = 0 → x = 0.

Estimated changes

Modified Mathlib/Algebra/Order/Star/Basic.lean

added theorem mul_star_self_pos_iff

added theorem star_mul_self_pos_iff

Modified Mathlib/Algebra/Star/Basic.lean

added theorem mul_star_self_eq_zero

added theorem mul_star_self_ne_zero

added theorem star_mul_self_eq_zero

added theorem star_mul_self_ne_zero

Modified Mathlib/Analysis/CStarAlgebra/Basic.lean

deleted theorem CStarRing.mul_star_self_eq_zero_iff

deleted theorem CStarRing.mul_star_self_ne_zero_iff

deleted theorem CStarRing.star_mul_self_eq_zero_iff

deleted theorem CStarRing.star_mul_self_ne_zero_iff

Modified Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

modified theorem Matrix.dotProduct_self_star_pos_iff

modified theorem Matrix.self_mul_conjTranspose_eq_zero

modified theorem dotProduct_self_star_eq_zero

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

modified theorem Matrix.PosDef.conjTranspose_mul_self

modified theorem Matrix.PosDef.mul_conjTranspose_self

modified theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff

modified theorem Matrix.PosSemidef.toLinearMap₂'_zero_iff