TensorSphere.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The real tensor criterion implies ordinary Euclidean cosphericity. The two constant/spatial matrix blocks are added to obtain the linear coefficient; no symmetry of the tensor matrix is assumed.

theorem OAI.EuclideanRamsey.realCriterion_cospherical line 18
Source documentation
The real tensor criterion places every point on one ordinary Euclidean sphere.
```
theorem realCriterion_cospherical {s d : ℕ} (a : Fin s → Space d)
    (hs : 0 < s) (h : RealCriterion a) :
    EuclideanGeometry.Cospherical (Set.range a) := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.RealCriterion