OAI/NumberTheory/Ostmann/Characters/FiniteKernelLinearMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Linear maps for the concrete finite kernel blocks

  1. def OAI.Ostmann.centeredSupportLinearMap line 10
  2. def OAI.Ostmann.rawKernelLinearMap line 23
  3. def OAI.Ostmann.residueLowerLinearMap line 35
  4. def OAI.Ostmann.polydiscLowerLinearMap line 39
  5. theorem OAI.Ostmann.polydiscLowerLinearMap_apply line 44
  6. theorem OAI.Ostmann.residuePointVector_expansion line 48
  7. theorem OAI.Ostmann.finiteLinearMap_point_expansion line 53