OAI/GroupTheory/PolycyclicRecognition/Analysis/LinearDeterminantMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.abs_det_eq_one_of_measurePreserving_linearMap line 14
2. theorem OAI.PolycyclicRecognition.abs_det_eq_one_of_measurePreserving line 30
3. theorem OAI.PolycyclicRecognition.det_eq_restrict_of_quotient_eq_id line 38
4. theorem OAI.PolycyclicRecognition.abs_det_eq_one_of_kernel_volume line 46

   Source documentation

   Volume preservation on a kernel and the identity action on its quotient force the full determinant to have absolute value one.

   theorem abs_det_eq_one_of_kernel_volume (U : Submodule ℝ V)
       (F : V →ₗ[ℝ] V) (hF : F.det ≠ 0) (hU : U ≤ U.comap F)
       (hquot : U.mapQ U F hU = LinearMap.id)
       {n : ℕ} (b : Module.Basis (Fin n) ℝ U)
       (hvol : MeasurePreserving (b.equivFun.conj (F.restrict hU)) volume volume) :
       |F.det| = 1 := by
   …