OAI/GroupTheory/PolycyclicRecognition/Geometry/RealShadowOperators.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The triangular operator underlying the real shadow adjoint action

  1. def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightCorrectedOperator line 19
  2. def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightCorrectedOperator line 22
  3. theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightCorrectedOperator_complexify line 27
  4. theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightCorrectedOperator_upper line 45
  5. theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightCorrectedOperator_diagonal_im line 54

    Source documentation

    The corrected operator has real diagonal in the original complex flag.

    theorem complexWeightCorrectedOperator_diagonal_im (x : L) (i : Fin n) :
    (LinearMap.toMatrix T.basis T.basis (T.complexWeightCorrectedOperator H x) i i).im = 0 := by
…