OAI/GroupTheory/PolycyclicRecognition/Geometry/HeightKernelDeterminant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unimodularity and the determinant of the actual adjoint action

The kernel is measured in exponential coordinates. Conjugation preserves that measure by the quotient-section argument, and acts as the identity on the height quotient. The two determinant factors therefore have absolute value one.

  1. theorem OAI.PolycyclicRecognition.abs_det_conjugationDifferential_eq_one_of_height_coordinates line 28