Pretty printing `inner`, and argument explicitness

Stream: mathlib4

[Jovan Gerbscheid]

At #24473 I wrote a delaborator for pretty printing inner, because when working with real inner products, it's really annoying to not see the ⟪x, y⟫ notation. However, I found out it's not necessary to write a delaborator: we can use the automatically generated unexpander, if inner takes 𝕜 as an explicit argument. This is now possible thank's to the feature added by @Kyle Miller. So should we make this change?

[Jireh Loreaux]

To be clear, what would happen with your proposal is the following:

1. 𝕜 becomes explicit in inner.
2. the notation ⟪x, y⟫_𝕜 inserts 𝕜 into the explicit (instead of the current implicit) slot
3. inner 𝕜 x y delaborates to ⟪x, y⟫_𝕜
4. within the scope of RealInnerProductSpace (resp. ComplexInnerProductSpace), ⟪x, y⟫ still elaborates to inner ℝ x y (resp. inner ℂ x y), but delaborates to ⟪x, y⟫_ℝ (resp. ⟪x, y⟫_ℂ). So you can still write ⟪x, y⟫ in the source, but there's no roundtripping.
5. due to (4), this essentially only affects delaboration, and very few changes are needed across Mathlib.

Is that an accurate summaary?

[Jireh Loreaux]

If so, :thumbs_up:

[Jovan Gerbscheid]

⟪x, y⟫_𝕜 is scoped notation inside InnerProductSpace, so it only pretty prints like that in that scope. So inner ℝ x y is printed as ⟪x, y⟫ when using it in its scope.

In the case that all scopes are open, we can choose which one we get by reordering the notation commands.

[Jovan Gerbscheid]

Do you think ⟪x, y⟫_𝕜 should be global notation? That seems reasonable to me.

[Eric Wieser]

Another option is to have a custom delaborator that shows inner (K := K) x y when K isn't real, and omits it otherwise

[Jovan Gerbscheid]

Do you mean in order to get the appExpanders to work?

[Jovan Gerbscheid]

Eric Wieser said:

Another option is to have a custom delaborator that shows inner (K := K) x y when K isn't real, and omits it otherwise

I don't see how that's better than having 𝕜 as an explicit argument

[Jireh Loreaux]

Sorry, I meant that the InnerProductSpace notation stays in that scope.

[Jovan Gerbscheid]

#24499 makes the argument explicit