Real Tensor Proof Toolkit

This file is the ℝ-specialized proof-facing companion to the spec tensor layer.

The tensor proof folder has two layers:

• NN.Proofs.Tensor.Algebra is backend-generic and proves semiring facts about recursive tensor dot products and executable folds.
• this file works in Spec over ℝ, where calculus, norms, Frobenius products, and model-analysis lemmas live.

The statements are intentionally PyTorch-shaped where that helps readers:

• flattenR / unflattenR give a Fin (Shape.size s) → ℝ view of Tensor ℝ s.
• lemmas relate toVec views to add_spec, scale_spec, etc.

We re-export selected generic helpers from NN.Proofs.Tensor.Algebra into the Spec.* namespace so downstream proof files can use one consistent tensor vocabulary (Spec.toVec, Spec.ofVec, Spec.finRange_foldl_add_eq_finset_sum) through shared fold and vector lemmas.

PyTorch correspondence / citations

• Flatten / reshape: torch.flatten, torch.reshape, and Tensor.view. https://pytorch.org/docs/stable/generated/torch.flatten.html https://pytorch.org/docs/stable/generated/torch.reshape.html https://pytorch.org/docs/stable/generated/torch.Tensor.view.html
• “numel”: tensor.numel() corresponds to Shape.size. https://pytorch.org/docs/stable/generated/torch.Tensor.numel.html

Algebraic instances for small tensor shapes

@[implicit_reducible]

instance Spec.instAddCommMonoidTensorRealScalar : AddCommMonoid (Tensor ℝ Shape.scalar)

Additive commutative monoid structure on scalar-shaped real tensors, transported by equivalence.

@[implicit_reducible]

instance Spec.instAddCommMonoidTensorRealDimScalar {n : ℕ} : AddCommMonoid (Tensor ℝ (Shape.dim n Shape.scalar))

Additive commutative monoid structure on 1D real tensors (transported via an equiv).

@[implicit_reducible]

instance Spec.instModuleRealTensorScalar {α : Type} [AddCommMonoid α] [Module ℝ α] : Module ℝ (Tensor α Shape.scalar)

Scalar tensors inherit an ℝ-module structure when their entries do, transported by equivalence.

@[implicit_reducible]

instance Spec.instModuleRealTensorDimScalar {α : Type} [AddCommMonoid α] [Module ℝ α] {n : ℕ} : Module ℝ (Tensor α (Shape.dim n Shape.scalar))

Tensor α (dim n scalar) inherits an ℝ-module structure when α is an ℝ-module (via an equiv).

@[implicit_reducible]

noncomputable instance Spec.instModuleRealTensorScalar_1 : Module ℝ (Tensor ℝ Shape.scalar)

Noncomputable ℝ-module instance on scalar real tensors (for calculus proofs).

@[implicit_reducible]

noncomputable instance Spec.instModuleRealTensorDimScalar_1 {n : ℕ} : Module ℝ (Tensor ℝ (Shape.dim n Shape.scalar))

Noncomputable ℝ-module instance on 1D real tensors (for calculus proofs).

1D helpers

theorem Spec.toVec_add_spec {n : ℕ} (x y : Tensor ℝ (Shape.dim n Shape.scalar)) : toVec (x.addSpec y) = fun (i : Fin n) => toVec x i + toVec y i

toVec distributes over pointwise addition (add_spec).

theorem Spec.toVec_scale_spec {n : ℕ} (x : Tensor ℝ (Shape.dim n Shape.scalar)) (c : ℝ) : toVec (x.scaleSpec c) = fun (i : Fin n) => toVec x i * c

toVec distributes over pointwise scaling (scale_spec).

def Spec.flattenR {s : Shape} (x : Tensor ℝ s) : Fin s.size → ℝ

Flatten a tensor of shape s into a 1D view Fin (Shape.size s) → ℝ.

This is the proof-facing counterpart of Spec.Tensor.flatten_spec specialized to ℝ. In PyTorch terms it is the functional analogue of flattening a tensor and then indexing it linearly (torch.flatten, tensor.view(-1)). See the spec file NN/Spec/Core/TensorReductionShape.lean for the definitional flatten/unflatten interface.

Citations: https://pytorch.org/docs/stable/generated/torch.flatten.html https://pytorch.org/docs/stable/generated/torch.Tensor.view.html

def Spec.unflattenR {s : Shape} (v : Fin s.size → ℝ) : Tensor ℝ s

Unflatten a 1D view Fin (Shape.size s) → ℝ back into a tensor of shape s.

This is the proof-facing counterpart of Spec.Tensor.unflatten_spec specialized to ℝ, and is intended to round-trip with flattenR under the spec lemmas in NN/Spec/Core/TensorReductionShape.lean.

Pointwise tensor algebra

theorem Spec.mul_spec_assoc {s : Shape} (a b c : Tensor ℝ s) : a.mulSpec (b.mulSpec c) = (a.mulSpec b).mulSpec c

Elementwise multiplication is associative (mul_spec is pointwise (*)).

theorem Spec.mul_spec_comm {s : Shape} (a b : Tensor ℝ s) : a.mulSpec b = b.mulSpec a

Elementwise multiplication is commutative (mul_spec is pointwise (*)).

theorem Spec.add_spec_comm {s : Shape} (a b : Tensor ℝ s) : a.addSpec b = b.addSpec a

Elementwise addition is commutative (add_spec is pointwise (+)).

theorem Spec.mul_spec_fill_zero {s : Shape} : (fill 0 s).mulSpec (fill 0 s) = fill 0 s

Elementwise multiplication of two all-zero tensors is the all-zero tensor.

Real dot product and fold bridges

noncomputable def Spec.dot {s : Shape} (a b : Tensor ℝ s) : ℝ

Real dot product for same-shape tensors, defined as the sum of elementwise products.

This matches the common PyTorch idiom (a * b).sum() for same-shape tensors. Citations: https://pytorch.org/docs/stable/generated/torch.sum.html

This is the Spec-namespace dot product used by real-analysis proofs. The backend-generic recursive dot product is Proofs.TensorAlgebra.dot.

theorem Spec.tensor_foldl_spec_go_of_lt {α β : Type} (f : β → α → β) {n : ℕ} {s : Shape} (values : Fin n → Tensor α s) {k : ℕ} (acc : β) (hk : k < n) : Tensor.tensorFoldlSpec.go f n s values k acc = Tensor.tensorFoldlSpec.go f n s values (k + 1) (Tensor.tensorFoldlSpec f acc (values ⟨k, hk⟩))

One-step unfolding of the internal tail-recursive helper tensor_foldl_spec.go when the loop condition holds (k < n).

This lemma is a proof tool: it lets proofs peel one loop step without using unfold directly.

theorem Spec.tensor_foldl_spec_go_of_not_lt {α β : Type} (f : β → α → β) {n : ℕ} {s : Shape} (values : Fin n → Tensor α s) {k : ℕ} (acc : β) (hk : ¬k < n) : Tensor.tensorFoldlSpec.go f n s values k acc = acc

One-step unfolding of the internal tail-recursive helper tensor_foldl_spec.go when the loop condition fails (¬ k < n), i.e. the loop terminates and returns the accumulator.

theorem Spec.tensor_foldl_spec_add_init {s : Shape} (acc : ℝ) (t : Tensor ℝ s) : Tensor.tensorFoldlSpec (fun (x1 x2 : ℝ) => x1 + x2) acc t = acc + t.sumSpec

Accumulator lemma for tensor_foldl_spec specialized to addition.

Informally: folding with (+) over a tensor adds sum_spec t to the initial accumulator. This is frequently used to move between “fold-style” specs and “sum-style” algebra.

theorem Spec.dot_mul_reassoc {s : Shape} (dLdy m dx : Tensor ℝ s) : dot dLdy (m.mulSpec dx) = dot (m.mulSpec dLdy) dx

Reassociate a dot over a pointwise product, using commutativity/associativity of mul_spec.

theorem Spec.get2_eq {α : Type} {m n : ℕ} (A : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))) (i : Fin m) (j : Fin n) : get2 A i j = match get A i with | Tensor.dim row => match row j with | Tensor.scalar v => v

Unfolding lemma for get2 (2D tensor indexing).

theorem Spec.get_eq {α : Type} {n : ℕ} {s : Shape} (t : Tensor α (Shape.dim n s)) (i : Fin n) : get t i = match t with | Tensor.dim f => f i

Unfolding lemma for get on a Tensor.dim value.

theorem Spec.toVec_mat_vec_mul_spec {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (v : Tensor ℝ (Shape.dim n Shape.scalar)) (i : Fin m) : toVec (matVecMulSpec A v) i = ∑ k : Fin n, get2 A i k * toVec v k

Coordinate formula for mat_vec_mul_spec, converted from the spec's List.finRange fold to a Finset.univ.sum.

This is the “PyTorch-looking” statement of matvec: each output entry is a dot product of the corresponding row with the input vector.

theorem Spec.get2_mat_mul_spec {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (i : Fin m) (j : Fin p) : get2 (matMulSpec A B) i j = ∑ k : Fin n, get2 A i k * get2 B k j

Coordinate formula for mat_mul_spec (matrix-matrix multiplication).

This is the standard triple-sum identity: (A @ B)[i,j] = ∑ k, A[i,k] * B[k,j], matching the textbook/PyTorch view of matrix multiplication.

Citations: https://pytorch.org/docs/stable/generated/torch.matmul.html

theorem Spec.sum_spec_dim {n : ℕ} {s : Shape} (t : Tensor ℝ (Shape.dim n s)) : t.sumSpec = ∑ i : Fin n, (get t i).sumSpec

Sum over the outer dimension unfolds into a Finset.univ sum of inner sum_spec.

This is the tensor analogue of torch.sum reducing over a leading dimension.

theorem Spec.sum_spec_vec {n : ℕ} (v : Tensor ℝ (Shape.dim n Shape.scalar)) : v.sumSpec = ∑ i : Fin n, toVec v i

sum_spec on a 1D tensor equals the Finset sum of its coordinates (toVec).

theorem Spec.toVec_mul_spec {n : ℕ} (a b : Tensor ℝ (Shape.dim n Shape.scalar)) (i : Fin n) : toVec (a.mulSpec b) i = toVec a i * toVec b i

toVec of mul_spec is pointwise multiplication of coordinate functions.

theorem Spec.dot_vec_eq_sum {n : ℕ} (a b : Tensor ℝ (Shape.dim n Shape.scalar)) : dot a b = ∑ i : Fin n, toVec a i * toVec b i

Dot product of vectors is the coordinate-wise sum ∑ i, a[i] * b[i].

theorem Spec.toVec_vec_mat_mul_spec {m n : ℕ} (v : Tensor ℝ (Shape.dim m Shape.scalar)) (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (j : Fin n) : toVec (vecMatMulSpec v A) j = ∑ i : Fin m, toVec v i * get2 A i j

Coordinate formula for vec_mat_mul_spec as a Finset sum: (v @ A)[j] = ∑ i, v[i] * A[i,j].

theorem Spec.dot_mat_linear_adjoint {inDim outDim : ℕ} (W : Tensor ℝ (Shape.dim outDim (Shape.dim inDim Shape.scalar))) (dLdy : Tensor ℝ (Shape.dim outDim Shape.scalar)) (dx : Tensor ℝ (Shape.dim inDim Shape.scalar)) : dot dLdy (matVecMulSpec W dx) = dot (vecMatMulSpec dLdy W) dx

Adjointness of matrix-vector and vector-matrix multiplication under the dot product: ⟪y, W x⟫ = ⟪y W, x⟫ (a.k.a. ⟪y, W x⟫ = ⟪Wᵀ y, x⟫ depending on conventions).

This is the algebraic heart of the linear-layer gradient rule.

theorem Spec.shapeOf_eq_shape {α : Type} {s : Shape} (t : Tensor α s) : shapeOf t = s

shapeOf recovers the shape already tracked in the tensor type.

This is a small bridge for proofs that move between value-level shape computations and type-indexed tensor operations.

theorem Spec.get_preserves_inner_shape {n : ℕ} {s : Shape} (t : Tensor ℝ (Shape.dim n s)) (i : Fin n) : shapeOf (get t i) = s

Indexing the outer dimension of a tensor exposes a subtensor with the declared inner shape.

Map and elementwise operation laws

theorem Spec.map_spec_id {s : Shape} (t : Tensor ℝ s) : Tensor.mapSpec id t = t

Functor identity law for map_spec: mapping id is a no-op.

theorem Spec.map_spec_comp {s : Shape} (f g : ℝ → ℝ) (t : Tensor ℝ s) : Tensor.mapSpec f (Tensor.mapSpec g t) = Tensor.mapSpec (f ∘ g) t

Functor law for map_spec: mapping g then f equals mapping f ∘ g.

theorem Spec.map_spec_add_distrib {s : Shape} (f : ℝ → ℝ) (a b : Tensor ℝ s) (h : ∀ (x y : ℝ), f (x + y) = f x + f y) : Tensor.mapSpec f (a.addSpec b) = (Tensor.mapSpec f a).addSpec (Tensor.mapSpec f b)

A scalar additivity law lifts pointwise through map_spec and add_spec.

theorem Spec.map2_spec_comm {s : Shape} (f : ℝ → ℝ → ℝ) (a b : Tensor ℝ s) (h : ∀ (x y : ℝ), f x y = f y x) : Tensor.map2Spec f a b = Tensor.map2Spec f b a

Commutativity transfer: if f is commutative, then map2_spec f is commutative on tensors.

Matrix and vector algebra

theorem Spec.mat_vec_assoc {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (x : Tensor ℝ (Shape.dim p Shape.scalar)) : matVecMulSpec A (matVecMulSpec B x) = matVecMulSpec (matMulSpec A B) x

Associativity of matrix-vector multiplication: A (B x) = (A B) x.

theorem Spec.matrix_transpose_involution {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) : A.matrixTransposeSpec.matrixTransposeSpec = A

Matrix transpose is an involution.

theorem Spec.get2_matrix_transpose_spec {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (i : Fin n) (j : Fin m) : get2 A.matrixTransposeSpec i j = get2 A j i

Coordinate rule for matrix_transpose_spec: (Aᵀ)[i,j] = A[j,i].

theorem Spec.matrix_ext {m n : ℕ} {A B : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))} : (∀ (i : Fin m) (j : Fin n), get2 A i j = get2 B i j) → A = B

Matrix extensionality: matrices are equal when all their entries are equal.

theorem Spec.matrix_transpose_mul {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) : (matMulSpec A B).matrixTransposeSpec = matMulSpec B.matrixTransposeSpec A.matrixTransposeSpec

Transpose of a product: (A ⬝ B)ᵀ = Bᵀ ⬝ Aᵀ.

theorem Spec.dot_mat_eq_sum {m n : ℕ} (A B : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) : dot A B = ∑ i : Fin m, ∑ j : Fin n, get2 A i j * get2 B i j

Expand the matrix dot-product as a double sum over entries (Frobenius inner product).

theorem Spec.dot_mat_mul_right_adjoint {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (C : Tensor ℝ (Shape.dim m (Shape.dim p Shape.scalar))) : dot (matMulSpec A B) C = dot A (matMulSpec C B.matrixTransposeSpec)

Right-adjointness of matrix multiplication under the Frobenius dot-product.

Informally: ⟪A ⬝ B, C⟫ = ⟪A, C ⬝ Bᵀ⟫.

theorem Spec.dot_mat_transpose {m n : ℕ} (A B : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) : dot A.matrixTransposeSpec B.matrixTransposeSpec = dot A B

Transpose invariance of the Frobenius dot-product: ⟪Aᵀ, Bᵀ⟫ = ⟪A, B⟫.

theorem Spec.dot_mat_mul_left_adjoint {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (C : Tensor ℝ (Shape.dim m (Shape.dim p Shape.scalar))) : dot (matMulSpec A B) C = dot B (matMulSpec A.matrixTransposeSpec C)

Left-adjointness of matrix multiplication under the Frobenius dot-product.

Informally: ⟪A ⬝ B, C⟫ = ⟪B, Aᵀ ⬝ C⟫.

theorem Spec.outer_product_transpose {m n : ℕ} (a : Tensor ℝ (Shape.dim m Shape.scalar)) (b : Tensor ℝ (Shape.dim n Shape.scalar)) : (outerProductSpec a b).matrixTransposeSpec = outerProductSpec b a

Outer product properties. Essential for proving weight gradient correctness.

Reductions and aggregation

theorem Spec.sum_spec_add_distrib {s : Shape} (a b : Tensor ℝ s) : (a.addSpec b).sumSpec = a.sumSpec + b.sumSpec

Sum distributes over elementwise addition.

theorem Spec.dot_comm {s : Shape} (a b : Tensor ℝ s) : dot a b = dot b a

Dot product properties. Essential for gradient computations and neural network training.

theorem Spec.dot_add_left {s : Shape} (a b c : Tensor ℝ s) : dot (a.addSpec b) c = dot a c + dot b c

Dot-product distributes over addition in the left argument.

theorem Spec.dot_scale_left {s : Shape} (a b : Tensor ℝ s) (k : ℝ) : dot (a.scaleSpec k) b = k * dot a b

Scaling a tensor scales its dot-product: dot (scale_spec a k) b = k * dot a b.

Flatten / unflatten round-trips

The round-trip lemmas for the spec definitions live with the definitions themselves: NN/Spec/Core/TensorReductionShape.lean provides

• Spec.Tensor.flatten_unflatten_inverse
• Spec.Tensor.unflatten_flatten_inverse

so downstream proof files do not need to re-prove the index arithmetic here.

theorem Spec.shape_size_add {s : Shape} (a b : Tensor ℝ s) : (shapeOf (a.addSpec b)).size = s.size

Size preservation under operations. Essential for proving tensor operations maintain expected dimensions.

theorem Spec.shape_size_mul {s : Shape} (a b : Tensor ℝ s) : (shapeOf (a.mulSpec b)).size = s.size

Size preservation for mul_spec: elementwise multiplication does not change shape size.

theorem Spec.safediv_bound {s : Shape} (a b : Tensor ℝ s) (_i : Fin s.size) : Numbers.epsilon > 0 → ∃ (bound : ℝ), (a.safedivSpec b).absSpec = Tensor.mapSpec (fun (x : ℝ) => min x bound) (a.safedivSpec b).absSpec

Existence of a uniform bound for safediv_spec, expressed via an idempotent min-clamp.

noncomputable def Spec.tensorNormSquared {s : Shape} (t : Tensor ℝ s) : ℝ

Tensor norm properties. Essential for regularization and optimization proofs.

theorem Spec.tensor_norm_squared_nonneg {s : Shape} (t : Tensor ℝ s) : tensorNormSquared t ≥ 0

tensor_norm_squared t is nonnegative, since it is a sum of squares.

theorem Spec.tensor_norm_squared_nonneg2 {s : Shape} (t : Tensor ℝ s) : 0 ≤ tensorNormSquared t

Convenience orientation of tensor_norm_squared_nonneg.

Keep this untagged as a simp lemma: the canonical theorem above uses the existing >= spelling, while downstream analysis proofs often need the 0 ≤ ... spelling for Real.sq_sqrt.

theorem Spec.tensor_norm_squared_zero_iff {s : Shape} (t : Tensor ℝ s) : tensorNormSquared t = 0 ↔ t = fill 0 s

tensor_norm_squared t = 0 iff t is the all-zero tensor.

Extensionality and structural algebra

theorem Spec.tensor_ext {α : Type} {s : Shape} {x y : Tensor α s} : (∀ (idxs : List ℕ), getSpec x idxs = getSpec y idxs) → x = y

Tensor extensionality over a generic element type: equal getSpec views imply equal tensors.

theorem Spec.add_spec_assoc {s : Shape} (a b c : Tensor ℝ s) : (a.addSpec b).addSpec c = a.addSpec (b.addSpec c)

Elementwise addition is associative (over ℝ tensors).

theorem Spec.sub_spec_add_right {s : Shape} (a b c : Tensor ℝ s) : a.subSpec (b.addSpec c) = (a.subSpec b).addSpec c.negSpec

Elementwise subtraction distributes over addition on the right.

theorem Spec.mul_spec_add_right {s : Shape} (a b c : Tensor ℝ s) : a.mulSpec (b.addSpec c) = (a.mulSpec b).addSpec (a.mulSpec c)

Elementwise multiplication distributes over addition on the right.

theorem Spec.mul_spec_add_left {s : Shape} (a b c : Tensor ℝ s) : (a.addSpec b).mulSpec c = (a.mulSpec c).addSpec (b.mulSpec c)

Elementwise multiplication distributes over addition on the left.

theorem Spec.sub_spec_bias_cancel {s : Shape} (a b c : Tensor ℝ s) : (a.addSpec c).subSpec (b.addSpec c) = a.subSpec b

Bias cancellation for tensor subtraction: (a + c) - (b + c) = a - b.

theorem Spec.mat_vec_add {m n : ℕ} (W : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (x y : Tensor ℝ (Shape.dim n Shape.scalar)) : matVecMulSpec W (x.addSpec y) = (matVecMulSpec W x).addSpec (matVecMulSpec W y)

Linearity of matrix-vector multiplication in the vector argument (addition).

theorem Spec.mat_vec_scale {m n : ℕ} (W : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (x : Tensor ℝ (Shape.dim n Shape.scalar)) (c : ℝ) : matVecMulSpec W (x.scaleSpec c) = (matVecMulSpec W x).scaleSpec c

Linearity of matrix-vector multiplication in the vector argument (scaling).

theorem Spec.mat_vec_linear_combination {m n : ℕ} (W : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (x y : Tensor ℝ (Shape.dim n Shape.scalar)) (a b : ℝ) : matVecMulSpec W ((x.scaleSpec a).addSpec (y.scaleSpec b)) = ((matVecMulSpec W x).scaleSpec a).addSpec ((matVecMulSpec W y).scaleSpec b)

Full linearity of matrix-vector multiplication in the vector argument.

@[simp]

theorem Spec.get_dim_scalar {n : ℕ} (f : Fin n → Tensor ℝ Shape.scalar) (i : Fin n) : get (Tensor.dim f) i = f i

Simplification lemmas for common patterns. Useful for automated proof tactics.

@[simp]

theorem Spec.toScalar_scalar (x : ℝ) : (Tensor.scalar x).toScalar = x

toScalar is the identity on scalar tensors.

theorem Spec.option_zero_add (o : Option ℝ) : Option.map (fun (x : ℝ) => 0 + x) o = o

Mapping 0 + · over an Option is the identity.

@[simp]

theorem Spec.add_spec_zero_left {s : Shape} (t : Tensor ℝ s) : (fill 0 s).addSpec t = t

Left identity for add_spec: adding the all-zero tensor does nothing.

@[simp]

theorem Spec.add_spec_zero_right {s : Shape} (t : Tensor ℝ s) : t.addSpec (fill 0 s) = t

Right identity for add_spec: adding the all-zero tensor does nothing.

@[simp]

theorem Spec.mul_spec_one_left {s : Shape} (t : Tensor ℝ s) : (fill 1 s).mulSpec t = t

Left identity for mul_spec: multiplying by the all-ones tensor does nothing.

@[simp]

theorem Spec.mul_spec_one_right {s : Shape} (t : Tensor ℝ s) : t.mulSpec (fill 1 s) = t

Right identity for mul_spec: multiplying by the all-ones tensor does nothing.