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_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

@[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

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 = LinearEquiv.of_relabel 𝕜 e

@[simp]

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

@[simp]

theorem LinearEquiv.euclidean_of_relabel_apply {d : Type u_1} {d₂ : Type u_3} (𝕜 : Type u_6) [RCLike 𝕜] (e : d ≃ d₂) (a✝ : d₂ → 𝕜) (b : d) : (euclidean_of_relabel 𝕜 e) a✝ b = (Equiv.piCongrLeft (fun (x : d) => 𝕜) e.symm) a✝ b

@[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)