OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularAdjointTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transporting a triangular adjoint basis through a Lie isomorphism

  1. def OAI.PolycyclicRecognition.TriangularAdjoint.comapLieEquiv line 14

    Source documentation

    The same adjoint matrices in the pulled-back basis.

    def TriangularAdjoint.comapLieEquiv (T : TriangularAdjoint K n) (e : L ≃ₗ⁅ℝ⁆ K) :
    TriangularAdjoint L n where
…

    Mentions: OAI.PolycyclicRecognition.TriangularAdjoint

  2. theorem OAI.PolycyclicRecognition.nonempty_triangularAdjoint_of_lieEquiv line 29