OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transporting support data to the chosen height coordinates

  1. def OAI.PolycyclicRecognition.SupportDatum.transport line 13

    Source documentation

    Change the linear coordinates on height, retaining the word multiplicities.

    def transport (D : PolycyclicRecognition.SupportDatum V I B) (e : V ≃ₗ[ℝ] W) :
    PolycyclicRecognition.SupportDatum W I B where
…

    Mentions: OAI.PolycyclicRecognition.SupportDatum

  2. theorem OAI.PolycyclicRecognition.SupportDatum.transport_weight_apply line 23