Standard euclidean space

Stream: mathlib4

[lennox]

What is the standard implementation of

$$\mathbb{R}^2$$

in mathlib? Neither

$$\mathbb{R} \times \mathbb{R}$$

nor

EuclideanSpace Real (Fin 2)

can be used for elementary operations such as angle, apparently because they are not AddCommGroups.

[Jireh Loreaux]

Can you make an #mwe ? These are definitely AddCommGroups. Are you wanting to use docs#InnerProductGeometry.angle, or something else?

[Jireh Loreaux]

This works in the live editor:

import Mathlib

#synth AddCommGroup (EuclideanSpace ℝ (Fin 2))

noncomputable
example (x y : EuclideanSpace ℝ (Fin 2)) := InnerProductGeometry.angle x y

[lennox]

Thank you! I had no idea about the #synth command -- I am very new to Lean.

[Eric Wieser]

When you have something that "apparently" doesn't work, it is very helpful to provide a #mwe or at least an error message; no one else with the same problem is likely to find this thread helpful if no one can tell what your actual problem was!