synthesize instance`InnerProductSpace ℝ (Fin 2 → ℝ)`

Stream: new members

[Moritz Firsching]

I'm trying to use ∠ for some very simple 2d geometry. However, I fail to make it work, and get a failed to synthesize instance error. I haven't tried much synthesizing an instance like that by hand, because I suspect, there could be a already a version of ℝ^2 that comes with an inner product. How to correctly talk about an angle in ℝ^2? What is the canonical type of that in mathlib?

import Mathlib
open EuclideanGeometry

example (a b c : Fin 2 → ℝ) : ∃ (β : ℝ), β = ∠ a b c := by
  sorry

example (a b c : ℝ × ℝ) : ∃ (β : ℝ), β = ∠ a b c := by
  sorry

[Patrick Massot]

EuclideanSpace ℝ (Fin 2)

[Patrick Massot]

will give you access to docs#EuclideanSpace.instInnerProductSpace

[Eric Wieser]

For the second one, you can use WithLp 2 (ℝ × ℝ)

[Eric Wieser]

(EuclideanSpace ℝ (Fin 2) is in fact a shorthand for WithLp 2 (Fin 2 → ℝ))

[Michael Stoll]

It is not actually shorter, though ...