Rotations in Fin 2 → ℝ

Stream: new members

[Anas Himmi]

Hi ! How can I define a rotation of a specific angle in Fin 2 → ℝ ? I tried the following :

def rot_neg_pi_div_4 (o : Orientation ℝ (Fin 2 → ℝ) (Fin 2)) : (Fin 2 → ℝ) ≃ₗᵢ[ℝ] (Fin 2 → ℝ) := o.rotation (-(π/4) : ℝ)

But it doesn't seem to work. I could define it from a matrix, but then I wouldn't get the linearEquiv for free. So what am I missing? Also, How can I define the direct orientation? I tried this :

def direct_orientation : Orientation ℝ (Fin 2 → ℝ) (Fin 2) := Basis.orientation ⟨Basis.ofRepr (LinearEquiv.refl _ _)⟩

But this also doesn't work.

Thank you in advance

[Aaron Liu]

import Mathlib

instance : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin n)) = n) where
  out := by rw [finrank_euclideanSpace, Fintype.card_fin]

noncomputable section

open Real

def rot_neg_pi_div_4 (o : Orientation ℝ (EuclideanSpace ℝ (Fin 2)) (Fin 2)) :
    (EuclideanSpace ℝ (Fin 2)) ≃ₗᵢ[ℝ] (EuclideanSpace ℝ (Fin 2)) :=
  o.rotation (.coe (-(π/4)))

[Eric Wieser]

I wonder if we should have that instance in mathlib? I've written it myself in the past

[Anas Himmi]

Thank you !