OAI/GroupTheory/PolycyclicRecognition/Algebra/MappedBasisBrackets.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coordinate bracket preservation under a Lie-algebra identification

  1. theorem OAI.PolycyclicRecognition.basisBracket_map_lieEquiv line 13

    Source documentation

    Mapping both the vectors and their basis leaves the coordinate Lie bracket unchanged.

    theorem basisBracket_map_lieEquiv
    {L L' : Type*} [LieRing L] [LieAlgebra ℝ L] [LieRing L'] [LieAlgebra ℝ L']
    {n : ℕ} (b : Basis (Fin n) ℝ L) (e : L ≃ₗ⁅ℝ⁆ L') :
    basisBracket (b.map e.toLinearEquiv) = basisBracket b := by
…

    Mentions: OAI.PolycyclicRecognition.basisBracket