def LinearEquiv.of_relabel {d : Type u_1} {d₂ : Type u_3} (R : Type u_7) [Semiring R] (e : d ≃ d₂) : (d₂ → R) ≃ₗ[R] d → R

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.of_relabel_apply {d : Type u_1} {d₂ : Type u_3} (R : Type u_7) [Semiring R] (e : d ≃ d₂) (a✝ : d₂ → R) (b : d) : (of_relabel R e) a✝ b = (Equiv.piCongrLeft (fun (x : d) => R) e.symm).toFun a✝ b

@[simp]

theorem LinearEquiv.of_relabel_symm_apply {d : Type u_1} {d₂ : Type u_3} (R : Type u_7) [Semiring R] (e : d ≃ d₂) (a✝ : d → R) (a : d₂) : (of_relabel R e).symm a✝ a = (Equiv.piCongrLeft (fun (x : d) => R) e.symm).invFun a✝ a

def LinearEquiv.euclidean_of_relabel {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) : EuclideanSpace 𝕜 d₂ ≃ₗ[𝕜] EuclideanSpace 𝕜 d

Equations

• LinearEquiv.euclidean_of_relabel 𝕜 e = (WithLp.linearEquiv 2 𝕜 ((i : d₂) → (fun (x : d₂) => 𝕜) i)).trans ((LinearEquiv.of_relabel 𝕜 e).trans (WithLp.linearEquiv 2 𝕜 (d → 𝕜)).symm)

@[simp]

theorem LinearEquiv.euclidean_of_relabel_symm_apply_ofLp {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) (a✝ : EuclideanSpace 𝕜 d) (i : d₂) : ((euclidean_of_relabel 𝕜 e).symm a✝).ofLp i = a✝.ofLp (e.symm i)

@[simp]

theorem LinearEquiv.euclidean_of_relabel_apply_ofLp {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) (a✝ : WithLp 2 ((i : d₂) → (fun (x : d₂) => 𝕜) i)) (a✝¹ : d) : ((euclidean_of_relabel 𝕜 e) a✝).ofLp a✝¹ = (Equiv.piCongrLeft (fun (x : d) => 𝕜) e.symm) a✝.ofLp a✝¹

@[simp]

theorem LinearEquiv.of_relabel_refl {d : Type u_1} {R : Type u_7} [Semiring R] : of_relabel R (Equiv.refl d) = refl R (d → R)

@[simp]

theorem LinearEquiv.euclidean_of_relabel_refl {d : Type u_1} {𝕜 : Type u_6} [RCLike 𝕜] : euclidean_of_relabel 𝕜 (Equiv.refl d) = refl 𝕜 (EuclideanSpace 𝕜 d)

theorem Matrix.reindex_toLin' {d : Type u_1} {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {R : Type u_7} [CommSemiring R] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ R) : toLin' ((reindex e f) M) = ↑(LinearEquiv.of_relabel R e.symm) ∘ₗ toLin' M ∘ₗ ↑(LinearEquiv.of_relabel R f)

theorem Matrix.reindex_toEuclideanLin {d : Type u_1} {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ 𝕜) : toEuclideanLin ((reindex e f) M) = ↑(LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ₗ toEuclideanLin M ∘ₗ ↑(LinearEquiv.euclidean_of_relabel 𝕜 f)

theorem Matrix.reindex_right_toLin' {d : Type u_1} {d₂ : Type u_3} {d₃ : Type u_4} {R : Type u_7} [CommSemiring R] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d ≃ d₂) (M : Matrix d₃ d R) : toLin' ((reindex (Equiv.refl d₃) e) M) = toLin' M ∘ₗ ↑(LinearEquiv.of_relabel R e)

theorem Matrix.reindex_right_toEuclideanLin {d : Type u_1} {d₂ : Type u_3} {d₃ : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] [Fintype d] [DecidableEq d] [Fintype d₂] [DecidableEq d₂] (e : d ≃ d₂) (M : Matrix d₃ d 𝕜) : toEuclideanLin ((reindex (Equiv.refl d₃) e) M) = toEuclideanLin M ∘ₗ ↑(LinearEquiv.euclidean_of_relabel 𝕜 e)

theorem Matrix.reindex_left_toLin' {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {R : Type u_7} [CommSemiring R] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (M : Matrix d₁ d₂ R) : ⇑(toLin' ((reindex e (Equiv.refl d₂)) M)) = ⇑(LinearEquiv.of_relabel R e.symm) ∘ ⇑(toLin' M)

theorem Matrix.reindex_left_toEuclideanLin {d₁ : Type u_2} {d₂ : Type u_3} {d₃ : Type u_4} {𝕜 : Type u_6} [RCLike 𝕜] [Fintype d₂] [DecidableEq d₂] (e : d₁ ≃ d₃) (M : Matrix d₁ d₂ 𝕜) : ⇑(toEuclideanLin ((reindex e (Equiv.refl d₂)) M)) = ⇑(LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ ⇑(toEuclideanLin M)