OAI/Geometry/Cannon/Conformal/FiniteB.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonMobius.finiteB line 21
  2. def OAI.CannonMobius.finiteA line 22
  3. lemma OAI.CannonMobius.finiteA_ne_zero line 23
  4. def OAI.CannonMobius.finiteNormalizer line 39
  5. lemma OAI.CannonMobius.finiteNormalizer_spec line 41
  6. lemma OAI.CannonMobius.finiteNormalizer_biholomorphic line 76
  7. def OAI.CannonMobius.finiteCenterRaw line 81
  8. lemma OAI.CannonMobius.center_finite line 84
  9. lemma OAI.CannonMobius.continuousAt_finiteCenterRaw line 101
  10. lemma OAI.CannonMobius.continuousAt_center_finite line 127
  11. lemma OAI.CannonMobius.continuous_center line 139
  12. def OAI.CannonMobius.ratio line 164
  13. lemma OAI.CannonMobius.ratio_of_ne line 165
  14. lemma OAI.CannonMobius.ratio_zero line 166
  15. lemma OAI.CannonMobius.ratio_scale line 167
  16. lemma OAI.CannonMobius.inv_ratio line 171
  17. lemma OAI.CannonMobius.continuousAt_ratio line 181
  18. abbrev OAI.CannonMobius.Mat line 197
  19. abbrev OAI.CannonMobius.Nonsingular line 198
  20. def OAI.CannonMobius.matrixFun line 200
  21. lemma OAI.CannonMobius.matrixFun_infty line 203
  22. lemma OAI.CannonMobius.matrixFun_coe line 204
  23. def OAI.CannonMobius.swapColumns line 207
  24. lemma OAI.CannonMobius.matrixFun_inv line 208
  25. lemma OAI.CannonMobius.matrix_nonzero line 220
  26. lemma OAI.CannonMobius.first_column_nonzero line 227
  27. lemma OAI.CannonMobius.swapColumns_det line 231
  28. lemma OAI.CannonMobius.matrixFun_continuous_finite line 234
  29. lemma OAI.CannonMobius.matrixFun_continuous line 254
  30. lemma OAI.CannonMobius.continuous_matrixFun line 277
  31. lemma OAI.CannonMobius.matrixFun_eq_smul line 286
  32. def OAI.CannonMobius.matrixHomeomorph line 291
  33. lemma OAI.CannonMobius.matrixHomeomorph_apply line 306
  34. lemma OAI.CannonMobius.matrixFun_triangular line 309
  35. lemma OAI.CannonMobius.matrixFun_general line 327
  36. lemma OAI.CannonMobius.matrixHomeomorph_biholomorphic line 359
  37. def OAI.CannonMobius.rowNorm line 376
  38. def OAI.CannonMobius.numerator line 377
  39. def OAI.CannonMobius.matrixCenterRaw line 378
  40. def OAI.CannonMobius.matrixEnergy line 379
  41. lemma OAI.CannonMobius.rowNorm_pos line 381
  42. def OAI.CannonMobius.matrixCenter line 389
  43. lemma OAI.CannonMobius.complex_gram line 392
  44. lemma OAI.CannonMobius.matrixEnergy_center line 399
  45. lemma OAI.CannonMobius.continuous_rowNorm line 411
  46. lemma OAI.CannonMobius.continuous_numerator line 412
  47. lemma OAI.CannonMobius.continuousAt_matrixCenterRaw line 413
  48. def OAI.CannonMobius.halfInclusion line 422
  49. lemma OAI.CannonMobius.continuous_halfInclusion line 423
  50. def OAI.CannonMobius.centerEnergy line 426
  51. lemma OAI.CannonMobius.continuous_centerEnergy line 427
  52. theorem OAI.CannonMobius.compact_matrix_parameters line 431
  53. def OAI.CannonMobius.affineMatrix line 473
  54. def OAI.CannonMobius.generalMatrix line 474
  55. lemma OAI.CannonMobius.affineMatrix_det line 475
  56. lemma OAI.CannonMobius.generalMatrix_det line 476
  57. lemma OAI.CannonMobius.affineMatrix_fun line 479
  58. lemma OAI.CannonMobius.generalMatrix_fun line 484
  59. lemma OAI.CannonMobius.affineMatrix_center line 502
  60. lemma OAI.CannonMobius.generalMatrix_center line 504
  61. lemma OAI.CannonMobius.center_normal_form line 527
  62. lemma OAI.CannonMobius.exists_center_matrix line 543
  63. def OAI.CannonMobius.rescale line 559
  64. lemma OAI.CannonMobius.rescale_det line 560
  65. lemma OAI.CannonMobius.rescale_rowNorm line 563
  66. lemma OAI.CannonMobius.rescale_numerator line 566
  67. lemma OAI.CannonMobius.rescale_matrixFun line 569
  68. lemma OAI.CannonMobius.rescale_center line 579
  69. lemma OAI.CannonMobius.exists_normalized_matrix line 589
  70. lemma OAI.CannonMobius.exists_normalized_triple_matrix line 599
  71. lemma OAI.CannonMobius.compact_center_preimage line 609
  72. lemma OAI.CannonMobius.proper_center line 639