OAI/NumberTheory/Ostmann/Supply/LocalBlock.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Supply.LocalCoordinates line 12
2. def OAI.Ostmann.Supply.coordinateLift line 14
3. def OAI.Ostmann.Supply.coordinateExtract line 20
4. def OAI.Ostmann.Supply.localBlock line 24
5. theorem OAI.Ostmann.Supply.coordinateLift_apply line 28
6. theorem OAI.Ostmann.Supply.coordinateExtract_fst line 31
7. theorem OAI.Ostmann.Supply.coordinateExtract_snd line 34
8. theorem OAI.Ostmann.Supply.localBlock_fst line 37
9. theorem OAI.Ostmann.Supply.localBlock_snd line 44
10. theorem OAI.Ostmann.Supply.localBlock_add line 51
11. theorem OAI.Ostmann.Supply.localBlock_smul line 56