norm of orthonormal basis

Stream: Is there code for X?

[Rémy Degenne]

Do we have the fact that the norm of an element of an orthonormal basis is 1?
I expected the following examples to be simplified by simp, but now I can't even find a result that applies:

import Mathlib.Analysis.InnerProductSpace.PiL2

example {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E) (i : Fin (Module.finrank ℝ E)) :
    ‖b i‖ = 1 := by
  sorry

example {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (i : Fin (Module.finrank ℝ E)) :
    ‖stdOrthonormalBasis ℝ E i‖ = 1 := by
  sorry

[Rémy Degenne]

I looked at how those bases are defined, and the first example is proved simply by exact b.orthonormal.1 i. The second is a consequence of the first. Problem solved.
But we are missing the API lemma for that (which should be simp).

[Yaël Dillies]

Maybe the lemma isn't simp because it has a weak key of norm _?

[Rémy Degenne]

As far as I can tell there is no lemma? So it can't be simp.
You have to unpack the def of Orthonormal to find it. I'll make a PR with a simp lemma.

[Rémy Degenne]

#23332