Euclidean space

Stream: Is there code for X?

[Tianchen Zhao]

I want to use definitions of Euclidean inner product and Euclidean norm(L2) in ℝ × ℝ. I saw in analysis.normed_space.pi_Lp there is a nice defintion for Euclidean space that fits my requirement, but is there a way to apply these defs to ℝ × ℝ rather than euclidean_space ℝ (fin 2) ? Because I already prove many results based on ℝ × ℝ.

[Heather Macbeth]

Nope, not easily. The group proving the formula for the area of a disc had the same problem.

[Heather Macbeth]

https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/9_area_of_a_circle.lean