Commit 2025-03-13 16:19 471641b2

refactor: change ⟪x, y⟫_𝕜 := conj x * y to y * conj x. (#22715) This PR changes the definition of the instance InnerProductSpace 𝕜 𝕜 so that the inner field is defined as y * conj x instead of the current conj x * y. Note that this propositionally equal, but not definitionally equal, to the original. In particular, this is still conjugate linear in the first variable, and linear in the second variable. However, it does mean that for x y : ℝ, there is the slightly unexpected defeq ⟪x, y⟫_ℝ := y * x. The reason for this change is as follows. In C⋆-algebra theory, a CStarModule is a generalization of InnerProductSpace where the scalars are replaced by a C⋆-algebra. In the literature, we generally consider these as right A-modules (where A is the C⋆-algebra), which is why CStarModule is currently set up with SMul Aᵐᵒᵖ E. However, we will need both left and right C⋆-modules, which means we need to accept a SMul A E hypothesis instead. Any C⋆-algebra A is a (left) C⋆-module over itself via ⟪x, y⟫_A := y * star x. Because of noncommutativity, we need it to be in this order for the left action ⟪x, a • y⟫_A = a * ⟪x, y⟫_A. However, when A := ℂ, this would lead to conflicting (non-defeq) Inner ℂ ℂ instances with the current definition of InnerProductSpace 𝕜 𝕜. See the Zulip thread for further discussion.