OAI/NumberTheory/Ostmann/Supply/LocalKernelPolynomial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.scalarOnly line 12
2. theorem OAI.Ostmann.Supply.scalarOnly_fst line 17
3. theorem OAI.Ostmann.Supply.scalarOnly_snd line 21
4. theorem OAI.Ostmann.Supply.localBlock_constant_eq_scalarOnly line 24
5. theorem OAI.Ostmann.Supply.eval_four_single line 34
6. theorem OAI.Ostmann.Supply.collect_scalar_pencil line 44
7. def OAI.Ostmann.Supply.localKernelPolynomial line 49
8. theorem OAI.Ostmann.Supply.eval_localKernelPolynomial line 56
9. theorem OAI.Ostmann.Supply.localKernelPolynomial_zero line 73