OAI/GroupTheory/PolycyclicRecognition/Algebra/TemplateInverseRays.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Locating each source generator in the pulled-back target rays

  1. theorem OAI.PolycyclicRecognition.templateSymmetry_inverse_weight_ray line 15

    Source documentation

    Apply the ray theorem to the inverse symmetry. This identifies the target ray whose pullback contains any specified source generator.

    theorem templateSymmetry_inverse_weight_ray
    (D : SupportDatum W I B) (A : templateSymmetryGroup D)
    (j : I) (hj : D.weight j ≠ 0) :
    ∃ (i : I) (c : ℝ), 0 < c ∧ (D.weight i).comp A.val.toLinearMap = c • D.weight j := by
…

    Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup