OAI/NumberTheory/Ostmann/Arithmetic/MovingSumFactors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A shared dependent Fourier family for disjoint prime lists

  1. def OAI.Ostmann.movingSumFactors line 10

    Source documentation

    The dependent disjoint union of two families, with its motive explicit.

    def movingSumFactors {J I : Type*} (Q : J → ℕ) (L : I → ℕ)
    (gQ : ∀ j, ZMod (Q j) → ℂ) (gL : ∀ i, ZMod (L i) → ℂ) :
    ∀ i, ZMod (Sum.elim Q L i) → ℂ :=
…