Commit 2025-11-05 17:51 7c0491be

View on Github →

chore: rename conjugate to star_left_conjugate (#30692) We change _conjugate_ and _conjugate_' to _star_left_conjugate_ and _star_right_conjugate_ to avoid confusion since sometimes in some files the non-primed version means _ * _ * star _ and in others it means star _ * _ * _. In particular, Algebra/Algebra/StrictPositivity:

IsUnit.isStrictlyPositive_conjugate_iff -> IsUnit.isStrictlyPositive_star_right_conjugate_iff
IsUnit.isStrictlyPositive_conjugate_iff' -> IsUnit.isStrictlyPositive_star_left_conjugate_iff Algebra/Order/Star/Basic:
conjugate_nonnneg -> star_left_conjugate_nonneg
conjugate_nonneg' -> star_right_conjugate_nonneg
conjugate_le_conjugate -> star_left_conjugate_le_conjugate
conjugate_le_conjugate' -> star_right_conjugate_le_conjugate
conjugate_lt_conjugate -> star_left_conjugate_lt_conjugate
conjugate_lt_conjugate' -> star_right_conjugate_lt_conjugate
conjugate_pos -> star_left_conjugate_pos
conjugate_pos' -> star_right_conjugate_pos
IsUnit.conjugate_nonneg_iff -> IsUnit.star_right_conjugate_nonneg_iff
IsUnit.conjugate_nonneg_iff' -> IsUnit.star_left_conjugate_nonneg_iff Analysis/CStarAlgebra/CFC/Order:
CStarAlgebra.conjugate_le_norm_smul -> CStarAlgebra.star_left_conjugate_le_norm_smul
CStarAlgebra.conjugate_le_norm_smul' -> CStarAlgebra.star_right_conjugate_le_norm_smul LinearAlgebra/Matrix/PosDef:
Matrix.IsUnit.posSemidef_conjugate_iff -> Matrix.IsUnit.posSemidef_star_right_conjugate_iff
Matrix.IsUnit.posSemidef_conjugate_iff' -> Matrix.IsUnit.posSemidef_star_left_conjugate_iff
Matrix.IsUnit.posDef_conjugate_iff -> Matrix.IsUnit.posDef_star_right_conjugate_iff
Matrix.IsUnit.posDef_conjugate_iff' -> Matrix.IsUnit.posDef_star_left_conjugate_iff