OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkPrincipalSourceReindexWitnessBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.leftDraws line 25
2. abbrev OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.rightDraws line 27
3. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.blockJacobian line 30
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.blockJacobian_ne_zero line 33
5. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.choicePatternValue_of_valid line 36
6. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.fibreChoiceTest line 56
7. def OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.fibrePatternValue line 61
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.fibrePatternValue_eq_wholeMean line 64
9. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.primeChoicePatternValue_eq_wholeMean line 71
10. theorem OAI.Ostmann.Arithmetic.HistoryBulkPrincipalSourceReindexWitness.mixedChoicePatternValue_eq_wholeMean line 81