Linear Isometry Equiv between different lins of a matrix

Stream: new members

[nemo]

I'm looking for a function like this

example [RCLike 𝕜]
    [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
    [NormedAddCommGroup W] [InnerProductSpace 𝕜 W]
    [NormedAddCommGroup V'] [InnerProductSpace 𝕜 V']
    [NormedAddCommGroup W'] [InnerProductSpace 𝕜 W']
    (v : OrthonormalBasis (Fin n) 𝕜 V)
    (w : OrthonormalBasis (Fin m) 𝕜 W)
    (v' : OrthonormalBasis (Fin n) 𝕜 V')
    (w' : OrthonormalBasis (Fin m) 𝕜 W')
    (A : Matrix (Fin m) (Fin n) 𝕜) :
  (e₁ : V ≃ₗᵢ[𝕜] V' ) ×' (e₂ : W ≃ₗᵢ[𝕜] W') ×'(
    e₂ ∘ₗ A.toLin v.toBasis w.toBasis = (A.toLin v'.toBasis w'.toBasis) ∘ₗ e₁
  ) := sorry

are there functions I can use directly for this

[Eric Wieser]

Here's a start:

import Mathlib

example [RCLike 𝕜]
    [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
    [NormedAddCommGroup W] [InnerProductSpace 𝕜 W]
    [NormedAddCommGroup V'] [InnerProductSpace 𝕜 V']
    [NormedAddCommGroup W'] [InnerProductSpace 𝕜 W']
    (v : OrthonormalBasis (Fin n) 𝕜 V)
    (w : OrthonormalBasis (Fin m) 𝕜 W)
    (v' : OrthonormalBasis (Fin n) 𝕜 V')
    (w' : OrthonormalBasis (Fin m) 𝕜 W')
    (A : Matrix (Fin m) (Fin n) 𝕜) :
    (e₁ : V ≃ₗᵢ[𝕜] V' ) ×' (e₂ : W ≃ₗᵢ[𝕜] W') ×'(
      e₂ ∘ₗ A.toLin v.toBasis w.toBasis = (A.toLin v'.toBasis w'.toBasis) ∘ₗ e₁
    ) :=
  ⟨v.repr.trans v'.repr.symm, w.repr.trans w'.repr.symm, by
    ext
    simp [Matrix.toLin_apply, map_sum w.repr, map_sum w'.repr.symm, map_smul w.repr, map_smul w'.repr.symm]
    congr! 3
    sorry⟩

[Eric Wieser]

Looks like some API is missing here