OAI/Geometry/QuadricBundles/SymmetricFlags.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.powerCoordinates line 12
  2. lemma OAI.QuadricCounterexample.powerCoordinates_change line 13
  3. lemma OAI.QuadricCounterexample.powerCoordinates_overlap line 17
  4. lemma OAI.QuadricCounterexample.UniformlyRegularOn.comp_power line 21
  5. lemma OAI.QuadricCounterexample.firstFactor_power line 27
  6. lemma OAI.QuadricCounterexample.secondFactor_power line 30
  7. def OAI.QuadricCounterexample.EqualizerData.flagFrame line 36
  8. def OAI.QuadricCounterexample.EqualizerData.flagChange line 42
  9. def OAI.QuadricCounterexample.EqualizerData.flagBasis line 54
  10. lemma OAI.QuadricCounterexample.EqualizerData.flagBasis_det_unit line 56
  11. lemma OAI.QuadricCounterexample.EqualizerData.flagBasis_regular line 58
  12. def OAI.QuadricCounterexample.EqualizerData.flagMatrix line 63
  13. lemma OAI.QuadricCounterexample.EqualizerData.flagMatrix_change line 67
  14. lemma OAI.QuadricCounterexample.EqualizerData.flagMatrix_regular line 69
  15. lemma OAI.QuadricCounterexample.EqualizerData.flagMatrix_self line 81
  16. lemma OAI.QuadricCounterexample.EqualizerData.flagMatrix_cocycle line 86
  17. lemma OAI.QuadricCounterexample.EqualizerData.flagMatrix_triangular line 100
  18. def OAI.QuadricCounterexample.flagDegree line 114
  19. lemma OAI.QuadricCounterexample.power_mul_inv_power line 119
  20. lemma OAI.QuadricCounterexample.flag_pen_scalar line 124
  21. lemma OAI.QuadricCounterexample.flag_residual_scalar line 140
  22. lemma OAI.QuadricCounterexample.flag_last_scalar line 148
  23. lemma OAI.QuadricCounterexample.EqualizerData.flagChange_graded line 156
  24. def OAI.QuadricCounterexample.EqualizerData.symmetricFlag line 174