OAI/GroupTheory/PolycyclicRecognition/Algebra/ExtremeTemplateLabels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual template labels agree along extreme directions

The positive homogeneous segment-support norm already removes scaling on a ray. No auxiliary invariant Euclidean norm is a premise of this theorem.

  1. theorem OAI.PolycyclicRecognition.SupportDatum.extreme_template_derivative_values_equal line 18