OAI/Topology/CoarseAssembly/RelativeTwoDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoarseAssembly.OperatorKTheory.diagonalTwoUnitary line 13
2. theorem OAI.CoarseAssembly.OperatorKTheory.diagonalTwoUnitary_relative line 27
3. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoMatrix_diagonal line 37
4. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoClass_diagonal line 54

   Source documentation

   Two diagonal relative unitaries represent the sum of their K₁ classes.

   theorem relativeTwoClass_diagonal (u v : unitary R)
       (hu : (u : R) - 1 ∈ S) (hv : (v : R) - 1 ∈ S) :
       relativeTwoClass S (diagonalTwoUnitary u v) (diagonalTwoUnitary_relative S u v hu hv) =
         relativeClass S u hu + relativeClass S v hv := by
   …

   Mentions: OAI.CoarseAssembly.OperatorKTheory.relativeTwoClass, OAI.CoarseAssembly.OperatorKTheory.diagonalTwoUnitary, OAI.CoarseAssembly.OperatorKTheory.diagonalTwoUnitary_relative, OAI.CoarseAssembly.OperatorKTheory.relativeClass