OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentLatticeInnerLogarithm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inner logarithms in the actual nilpotent lattice model

  1. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLinear_inner_log line 18

    Source documentation

    The finite logarithm of a lattice inner automorphism is exactly the inner Lie derivation, including its normalization at the lattice element.

    theorem automorphismLinear_inner_log (t : H) :
    nilpotentLog (C.automorphismLinear (MulAut.conj t) - 1) =
      LieAlgebra.ad ℝ C.carrier (C.equiv t) := by
…

    Mentions: OAI.PolycyclicRecognition.nilpotentLog