A Few Facts that Hold in Euclidean Spaces

The contents of this file should, in my opinion, be in Mathlib. I'm not sure about tagging them with simp, but they seem simpable... not sure about this.

The results in this section are relevant to my attempt to build a canonical lattice in Euclidean space. I got close, but there are certain results in Mathlib that better suit spaces of the form ι → ℝ (that is, Pi types that have not been endowed with the additional structure of the Euclidean inner product, norm, and metric). These are still nice results, though.

@[simp]

theorem EuclideanSpace.smul_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq ι] (i : ι) (r s : 𝕜) : s • single i r = single i (s * r)

Multiplying EuclideanSpace.single by scalars results in a EuclideanSpace.single.

@[simp]

theorem EuclideanSpace.smul_single_one {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq ι] (i : ι) (s : 𝕜) : s • single i 1 = single i s

@[simp]

theorem EuclideanSpace.sum_smul_single_one {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (v : ι → 𝕜) : ∑ i : ι, v i • single i 1 = v

@[simp]

theorem EuclideanSpace.sum_single {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (v : ι → 𝕜) : ∑ i : ι, single i (v i) = v

noncomputable def EuclideanSpace.ofIsEmpty {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [IsEmpty ι] : EuclideanSpace 𝕜 ι ≃ₗ[𝕜] ↥0

Equations

• EuclideanSpace.ofIsEmpty = LinearEquiv.ofFinrankEq (EuclideanSpace 𝕜 ι) ↥0 ⋯