OAI/GroupTheory/PolycyclicRecognition/Geometry/ComplexWeightFactorModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent and Cartan factors for a solvable group with complex weights

  1. structure OAI.PolycyclicRecognition.ComplexWeightFactorModel line 26

    Source documentation

    The concrete group part of the complex-weight Cartan model. The ambient overlap is retained, and all lifting conclusions refer to the actual map.

    structure ComplexWeightFactorModel where
…
  2. theorem OAI.PolycyclicRecognition.nonempty_complexWeightFactorModel line 58