LinearSupportSymmetries.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite symmetry conclusion does not require a preselected norm or topology on the finite-dimensional height quotient.

theorem OAI.PolycyclicRecognition.finite_linear_support_isometries line 20
Source documentation
The support norm supplies the topology used to prove finiteness. The result concerns the original algebraic linear equivalences.
```
theorem finite_linear_support_isometries (D : SupportDatum W I B) :
    Set.Finite {A : W ≃ₗ[ℝ] W | ∀ w, D.segmentSupport (A w) = D.segmentSupport w} := by
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum
def OAI.PolycyclicRecognition.linearSupportSymmetryGroup line 39
Source documentation
The algebraic finite group of possible segment-support symmetries.
```
def linearSupportSymmetryGroup (D : SupportDatum W I B) : Subgroup (W ≃ₗ[ℝ] W) where
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum
instance OAI.PolycyclicRecognition.(instance at line 48) line 48