Inner product localized notation is not displayed

Stream: new members

[Wojciech Nawrocki]

In the following file:

import analysis.inner_product_space.pi_L2
open_locale real_inner_product_space

variables x y z : euclidean_space ℝ (fin 2)

/- inner x y : ℝ -/
#check ⟪x, y⟫

We don't see the notation used in the #check output (and not in goals either). Am I doing something wrong or is this a Lean issue (lean 3.48.0, mathlib 56e4f0d51f)?