OAI/Geometry/QuadricBundles/PolynomialGeneration.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.QuadricCounterexample.PolynomialGeneration line 14
2. def OAI.QuadricCounterexample.PolynomialGeneration.matrix line 22
3. def OAI.QuadricCounterexample.PolynomialGeneration.recover line 24
4. lemma OAI.QuadricCounterexample.PolynomialGeneration.recover_matrix line 26
5. lemma OAI.QuadricCounterexample.PolynomialGeneration.matrix_injective line 28
6. lemma OAI.QuadricCounterexample.PolynomialGeneration.matrix_nonzero line 33
7. abbrev OAI.QuadricCounterexample.EqualizerData.SymmetricGeneratorIndex line 50
8. def OAI.QuadricCounterexample.EqualizerData.symmetricGeneratorValue line 51
9. lemma OAI.QuadricCounterexample.EqualizerData.symmetricGeneratorValue_regular line 55
10. def OAI.QuadricCounterexample.EqualizerData.localGeneratorMatrix line 64
11. lemma OAI.QuadricCounterexample.EqualizerData.localGeneratorMatrix_det_unit line 67
12. lemma OAI.QuadricCounterexample.EqualizerData.localGeneratorMatrix_regular line 83
13. def OAI.QuadricCounterexample.EqualizerData.generatorRecoveryValue line 87
14. lemma OAI.QuadricCounterexample.EqualizerData.generatorRecoveryValue_regular line 90
15. lemma OAI.QuadricCounterexample.EqualizerData.generatorRecoveryValue_leftInverse line 101
16. def OAI.QuadricCounterexample.EqualizerData.symmetricGeneration line 131
17. lemma OAI.QuadricCounterexample.EqualizerData.symmetricGeneration_matrix line 146
18. lemma OAI.QuadricCounterexample.EqualizerData.symmetricGeneratorValue_compatible line 150