OAI/Analysis/SymmetricDomains/HermPartUnit.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Release061.Hermitian.complex_smul_split line 34
  2. def OAI.Release061.Hermitian.complexLinear line 43
  3. def OAI.Release061.Hermitian.holPart line 52
  4. def OAI.Release061.Hermitian.hermPart line 56
  5. lemma OAI.Release061.Hermitian.holPart_add_left line 61
  6. lemma OAI.Release061.Hermitian.holPart_add_right line 68
  7. lemma OAI.Release061.Hermitian.holPart_real_left line 73
  8. lemma OAI.Release061.Hermitian.holPart_real_right line 79
  9. lemma OAI.Release061.Hermitian.holPart_I_left line 86
  10. lemma OAI.Release061.Hermitian.holPart_I_right line 93
  11. lemma OAI.Release061.Hermitian.holPart_smul_left line 99
  12. lemma OAI.Release061.Hermitian.holPart_smul_right line 106
  13. def OAI.Release061.Hermitian.holBilinear line 113
  14. lemma OAI.Release061.Hermitian.hermPart_add_left line 118
  15. lemma OAI.Release061.Hermitian.hermPart_add_right line 125
  16. lemma OAI.Release061.Hermitian.hermPart_real_left line 130
  17. lemma OAI.Release061.Hermitian.hermPart_real_right line 136
  18. lemma OAI.Release061.Hermitian.hermPart_I_left line 143
  19. lemma OAI.Release061.Hermitian.hermPart_I_right line 150
  20. lemma OAI.Release061.Hermitian.hermPart_smul_left line 156
  21. lemma OAI.Release061.Hermitian.hermPart_smul_right line 163
  22. lemma OAI.Release061.Hermitian.hermPart_conj line 172
  23. lemma OAI.Release061.Hermitian.quadratic_decomposition line 178
  24. lemma OAI.Release061.Hermitian.hermPart_diag_real line 184
  25. lemma OAI.Release061.Hermitian.hermPart_smul_both line 188
  26. lemma OAI.Release061.Hermitian.holPart_smul_both line 192
  27. lemma OAI.Release061.Hermitian.hermPart_zero line 198
  28. def OAI.Release061.Hermitian.symmetrize line 201
  29. lemma OAI.Release061.Hermitian.symmetrize_symm line 205
  30. lemma OAI.Release061.Hermitian.symmetrize_diag line 210
  31. def OAI.Release061.Hermitian.holContinuous line 218
  32. lemma OAI.Release061.Hermitian.holPart_analytic line 222
  33. lemma OAI.Release061.Hermitian.hermPart_unit line 228