OAI/GroupTheory/PolycyclicRecognition/Geometry/CommutingLiePowerLogarithms.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Commuting logarithms for finitely many commuting Lie automorphisms

A single positive power works for the entire finite family. The logarithms commute because each constructed logarithm commutes with the full commutant of its original automorphism.

  1. theorem OAI.PolycyclicRecognition.commuting_lie_automorphisms_have_power_logs line 16