OAI/GroupTheory/FiniteType/FiniteIdempotentDiagrams.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteIdempotentDiagrams.OrthogonalAdditive line 12
  2. abbrev OAI.FiniteIdempotentDiagrams.rankOne line 21
  3. lemma OAI.FiniteIdempotentDiagrams.rankOne_idem line 23
  4. lemma OAI.FiniteIdempotentDiagrams.rankOne_orthogonal line 27
  5. lemma OAI.FiniteIdempotentDiagrams.rankOne_difference line 31
  6. lemma OAI.FiniteIdempotentDiagrams.variation_constant line 61
  7. lemma OAI.FiniteIdempotentDiagrams.nsmul_variation line 84
  8. lemma OAI.FiniteIdempotentDiagrams.OrthogonalAdditive.transpose line 117
  9. abbrev OAI.FiniteIdempotentDiagrams.basisVector line 130
  10. abbrev OAI.FiniteIdempotentDiagrams.diagonalUnit line 131
  11. lemma OAI.FiniteIdempotentDiagrams.basisVector_pair line 134
  12. lemma OAI.FiniteIdempotentDiagrams.diagonalUnit_idem line 138
  13. lemma OAI.FiniteIdempotentDiagrams.diagonalUnit_orthogonal line 142
  14. lemma OAI.FiniteIdempotentDiagrams.nsmul_diagonal_eq line 146
  15. abbrev OAI.FiniteIdempotentDiagrams.Mat3 line 189
  16. lemma OAI.FiniteIdempotentDiagrams.orthogonal_sum_idem line 191
  17. lemma OAI.FiniteIdempotentDiagrams.three_diagonal_sum line 195
  18. lemma OAI.FiniteIdempotentDiagrams.orthogonalAdditive_one line 201
  19. structure OAI.FiniteIdempotentDiagrams.ThreeCopies line 225
  20. def OAI.FiniteIdempotentDiagrams.ThreeCopies.system line 235
  21. lemma OAI.FiniteIdempotentDiagrams.ThreeCopies.mem_system line 238
  22. lemma OAI.FiniteIdempotentDiagrams.ThreeCopies.diagonal_mem line 241
  23. lemma OAI.FiniteIdempotentDiagrams.ThreeCopies.system_finite line 244
  24. def OAI.FiniteIdempotentDiagrams.OrthogonalAdditiveOn line 250
  25. lemma OAI.FiniteIdempotentDiagrams.ThreeCopies.additive_copy line 254
  26. theorem OAI.FiniteIdempotentDiagrams.ThreeCopies.annihilates_one line 265
  27. def OAI.FiniteIdempotentDiagrams.contraction line 308
  28. def OAI.FiniteIdempotentDiagrams.oneByOne line 320
  29. def OAI.FiniteIdempotentDiagrams.matrixCopy line 329
  30. lemma OAI.FiniteIdempotentDiagrams.matrixCopy_diagonal line 339