chore: rename **conjugate** to **star_left_conjugate**

[themathqueen]

We change _conjugate_ to _star_left_conjugate_ and _conjugate_' to _star_right_conjugate_ to avoid confusion since sometimes in some files it 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

---

There are more to do, but will leave this for another PR.

[github-actions]

PR summary 32bd6c7c8c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsUnit.posSemidef_star_left_conjugate_iff
+ IsUnit.posSemidef_star_right_conjugate_iff
+ IsUnit.star_left_conjugate_nonneg_iff
+ IsUnit.star_right_conjugate_nonneg_iff
+ _root_.IsUnit.isStrictlyPositive_star_left_conjugate_iff
+ _root_.IsUnit.isStrictlyPositive_star_right_conjugate_iff
+ _root_.Matrix.IsUnit.posDef_star_left_conjugate_iff
+ _root_.Matrix.IsUnit.posDef_star_right_conjugate_iff
+ star_left_conjugate_le_conjugate
+ star_left_conjugate_le_norm_smul
+ star_left_conjugate_lt_conjugate
+ star_left_conjugate_nonneg
+ star_left_conjugate_pos
+ star_right_conjugate_le_conjugate
+ star_right_conjugate_le_norm_smul
+ star_right_conjugate_lt_conjugate
+ star_right_conjugate_nonneg
+ star_right_conjugate_pos
- IsUnit.conjugate_nonneg_iff
- IsUnit.conjugate_nonneg_iff'
- IsUnit.posSemidef_conjugate_iff
- IsUnit.posSemidef_conjugate_iff'
- _root_.IsUnit.isStrictlyPositive_conjugate_iff
- _root_.IsUnit.isStrictlyPositive_conjugate_iff'
- _root_.Matrix.IsUnit.posDef_conjugate_iff
- _root_.Matrix.IsUnit.posDef_conjugate_iff'

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[themathqueen]

@j-loreaux, I also renamed CStarAlgebra.conjugate_le_norm_smul to match this way, but I can change it back if you want.

[j-loreaux]

I wonder if we can do even better regarding naming in this regard. Perhaps star _ * _ * _ could be star_conjugate (or star_left_conjugate) and other could be conjugate_star (or star_right_conjugate).

[themathqueen]

I like the star_left_conjugate and the star_right_conjugate! Makes it very clear.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.