Theorems · Definition · abstract harmonic analysis
DiscreteConvolution.addFiber
{M : Type u_1} → [AddMonoid M] → M → Set (M × M)The fiber of addition at x: all pairs (a, b) with a + b = x.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.univproof · cited by 3,945
- AddMonoidstatement and proof · cited by 2,864
- Set.antidiagonalproof · cited by 11
Cited by13
Results whose statement or proof uses this declaration.
- DiscreteConvolution.addConvolutionproof · cited by 11
- DiscreteConvolution.AddConvolutionExistsAtproof · cited by 4
- DiscreteConvolution.AddConvolutionExistsAt.distrib_addproof · cited by 1
- DiscreteConvolution.AddConvolutionExistsAt.add_distribproof · cited by 1
- DiscreteConvolution.mem_addFiberstatement · cited by 0
- DiscreteConvolution.AddConvolutionExistsAt.vadd_convolutionproof · cited by 0
- DiscreteConvolution.zero_addConvolutionproof · cited by 0
- DiscreteConvolution.addConvolution_commproof · cited by 0
- DiscreteConvolution.addConvolution_indicator_zero_leftproof · cited by 0
- DiscreteConvolution.addConvolution_indicator_zero_rightproof · cited by 0
- DiscreteConvolution.addConvolution_zeroproof · cited by 0
- DiscreteConvolution.addFiber_zero_memstatement · cited by 0