Shortcut instances for real Euclidean spaces

EuclideanSpace ℝ (Fin n) unfolds to WithLp 2 (Fin n → ℝ), whose structures are transported one class at a time from the function space. The shortcuts below record the normed-space and inner-product instances, and the normed-space instances of the continuous linear maps between two such spaces; they apply to the three-dimensional physical space and to the planes used throughout this development.

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSeminormedAddCommGroup {n : ℕ} : SeminormedAddCommGroup (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSeminormedAddCommGroup = NormedAddCommGroup.toSeminormedAddCommGroup

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instAdd {n : ℕ} : Add (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instAdd = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instDistribSMul {n : ℕ} : DistribSMul ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instDistribSMul = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSeminormedAddGroup {n : ℕ} : SeminormedAddGroup (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSeminormedAddGroup = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instContinuousSub {n : ℕ} : ContinuousSub (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instTopologicalSpace {n : ℕ} : TopologicalSpace (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instTopologicalSpace = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instNeg {n : ℕ} : Neg (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instNeg = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instContinuousAdd {n : ℕ} : ContinuousAdd (EuclideanSpace ℝ (Fin n))

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instNormedSpace {n : ℕ} : NormedSpace ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instNormedSpace = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instAddZeroClass {n : ℕ} : AddZeroClass (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instAddZeroClass = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instNormedAddGroup {n : ℕ} : NormedAddGroup (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instNormedAddGroup = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instNormSMulClass {n : ℕ} : NormSMulClass ℝ (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instAddCommMonoid {n : ℕ} : AddCommMonoid (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instAddCommMonoid = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instContinuousSMul {n : ℕ} : ContinuousSMul ℝ (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instMulAction {n : ℕ} : MulAction ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instMulAction = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSub {n : ℕ} : Sub (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSub = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instNormedAddCommGroup {n : ℕ} : NormedAddCommGroup (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instNormedAddCommGroup = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instAddCommGroup {n : ℕ} : AddCommGroup (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instAddCommGroup = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSubNegMonoid {n : ℕ} : SubNegMonoid (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSubNegMonoid = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instPseudoMetricSpace {n : ℕ} : PseudoMetricSpace (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instPseudoMetricSpace = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instNorm {n : ℕ} : Norm (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instNorm = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instIsBoundedSMul {n : ℕ} : IsBoundedSMul ℝ (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instUniformSpace {n : ℕ} : UniformSpace (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instUniformSpace = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instDistribMulAction {n : ℕ} : DistribMulAction ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instDistribMulAction = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instZero {n : ℕ} : Zero (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instZero = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instIsUniformAddGroup {n : ℕ} : IsUniformAddGroup (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instModule {n : ℕ} : Module ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instModule = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instContinuousConstSMul {n : ℕ} : ContinuousConstSMul ℝ (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSMulZeroClass {n : ℕ} : SMulZeroClass ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSMulZeroClass = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instMulActionWithZero {n : ℕ} : MulActionWithZero ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instMulActionWithZero = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instMetricSpace {n : ℕ} : MetricSpace (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instMetricSpace = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instIsTopologicalAddGroup {n : ℕ} : IsTopologicalAddGroup (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instAddMonoid {n : ℕ} : AddMonoid (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instAddMonoid = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSMul {n : ℕ} : SMul ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSMul = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instContinuousNeg {n : ℕ} : ContinuousNeg (EuclideanSpace ℝ (Fin n))

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instAddGroup {n : ℕ} : AddGroup (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instAddGroup = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instSMulWithZero {n : ℕ} : SMulWithZero ℝ (EuclideanSpace ℝ (Fin n))

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instSMulWithZero = inferInstance

@[instance_reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instInnerProductSpace {n : ℕ} : InnerProductSpace ℝ (EuclideanSpace ℝ (Fin n))

Shortcut for the inner product space structure of a real Euclidean space.

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instInnerProductSpace = inferInstance

@[instance_reducible]

noncomputable instance NavierStokesAndEuler.EuclideanSpaceShortcut.instInner {n : ℕ} : Inner ℝ (EuclideanSpace ℝ (Fin n))

Shortcut for the inner product of a real Euclidean space.

Equations

• NavierStokesAndEuler.EuclideanSpaceShortcut.instInner = inferInstance

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instFiniteDimensional {n : ℕ} : FiniteDimensional ℝ (EuclideanSpace ℝ (Fin n))

Shortcut for the finite dimensionality of a real Euclidean space.

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instCompleteSpace {n : ℕ} : CompleteSpace (EuclideanSpace ℝ (Fin n))

Shortcut for the completeness of a real Euclidean space.

instance NavierStokesAndEuler.EuclideanSpaceShortcut.instProperSpace {n : ℕ} : ProperSpace (EuclideanSpace ℝ (Fin n))

Shortcut for the properness of a real Euclidean space.

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instNeg {n m : ℕ} : Neg (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instNeg = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instAddCommGroup {n m : ℕ} : AddCommGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instAddCommGroup = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instAddMonoid {n m : ℕ} : AddMonoid (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instAddMonoid = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instContinuousAdd {n m : ℕ} : ContinuousAdd (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSMul {n m : ℕ} : SMul ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSMul = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instContinuousConstSMul {n m : ℕ} : ContinuousConstSMul ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSMulZeroClass {n m : ℕ} : SMulZeroClass ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSMulZeroClass = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instDistribSMul {n m : ℕ} : DistribSMul ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instDistribSMul = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSeminormedAddGroup {n m : ℕ} : SeminormedAddGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSeminormedAddGroup = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instContinuousSub {n m : ℕ} : ContinuousSub (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instMulAction {n m : ℕ} : MulAction ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instMulAction = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instUniformSpace {n m : ℕ} : UniformSpace (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instUniformSpace = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instTopologicalSpace {n m : ℕ} : TopologicalSpace (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instTopologicalSpace = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instPseudoMetricSpace {n m : ℕ} : PseudoMetricSpace (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instPseudoMetricSpace = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSub {n m : ℕ} : Sub (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSub = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instAddCommMonoid {n m : ℕ} : AddCommMonoid (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instAddCommMonoid = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instNormSMulClass {n m : ℕ} : NormSMulClass ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSubNegMonoid {n m : ℕ} : SubNegMonoid (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSubNegMonoid = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instNorm {n m : ℕ} : Norm (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instNorm = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instNormedAddCommGroup {n m : ℕ} : NormedAddCommGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instNormedAddCommGroup = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instIsTopologicalAddGroup {n m : ℕ} : IsTopologicalAddGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instIsBoundedSMul {n m : ℕ} : IsBoundedSMul ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instDistribMulAction {n m : ℕ} : DistribMulAction ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instDistribMulAction = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instNormedAddGroup {n m : ℕ} : NormedAddGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instNormedAddGroup = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instMetricSpace {n m : ℕ} : MetricSpace (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instMetricSpace = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instAddGroup {n m : ℕ} : AddGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instAddGroup = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instContinuousNeg {n m : ℕ} : ContinuousNeg (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instModule {n m : ℕ} : Module ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instModule = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instAddZeroClass {n m : ℕ} : AddZeroClass (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instAddZeroClass = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSeminormedAddCommGroup {n m : ℕ} : SeminormedAddCommGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSeminormedAddCommGroup = NormedAddCommGroup.toSeminormedAddCommGroup

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instZero {n m : ℕ} : Zero (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instZero = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instIsUniformAddGroup {n m : ℕ} : IsUniformAddGroup (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instMulActionWithZero {n m : ℕ} : MulActionWithZero ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instMulActionWithZero = inferInstance

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instAdd {n m : ℕ} : Add (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instAdd = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.EuclideanOperatorShortcut.instNormedSpace {n m : ℕ} : NormedSpace ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instNormedSpace = inferInstance

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instContinuousSMul {n m : ℕ} : ContinuousSMul ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

@[reducible]

instance NavierStokesAndEuler.EuclideanOperatorShortcut.instSMulWithZero {n m : ℕ} : SMulWithZero ℝ (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m))

Equations

• NavierStokesAndEuler.EuclideanOperatorShortcut.instSMulWithZero = inferInstance