OAI/GroupTheory/PolycyclicRecognition/Analysis/TraceFromKernelHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Zero adjoint trace from unimodularity and nilpotent kernel coordinates

This proves the needed conclusion directly from Haar invariance. No formula identifying the modular character with an adjoint determinant is assumed.

  1. theorem OAI.PolycyclicRecognition.trace_ad_eq_zero_of_kernel_haar line 29