Theorems · Theorem · harmonic analysis
SchwartzMap.convolution.congr_simp
∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : RCLike 𝕜]
[inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
[inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : NormedAddCommGroup F₁] [inst_7 : NormedSpace ℂ F₁]
[inst_8 : NormedSpace 𝕜 F₁] [inst_9 : SMulCommClass ℂ 𝕜 F₁] [inst_10 : NormedAddCommGroup F₂]
[inst_11 : NormedSpace ℂ F₂] [inst_12 : NormedSpace 𝕜 F₂] [inst_13 : SMulCommClass ℂ 𝕜 F₂]
[inst_14 : NormedAddCommGroup F₃] [inst_15 : NormedSpace ℂ F₃] [inst_16 : NormedSpace 𝕜 F₃]
[inst_17 : SMulCommClass ℂ 𝕜 F₃] (B B_1 : F₁ →L[𝕜] F₂ →L[𝕜] F₃),
B = B_1 → SchwartzMap.convolution B = SchwartzMap.convolution B_1- Defined in
- Mathlib.Analysis.Fourier.Convolution
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 301 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- RingHom.idstatement and proof · cited by 18,349
- NormedAddCommGroupstatement and proof · cited by 15,752
- MeasurableSpacestatement and proof · cited by 13,106
- NormedSpacestatement and proof · cited by 12,499
- LinearMapstatement · cited by 10,215
- Complexstatement and proof · cited by 5,565
- ContinuousLinearMapstatement and proof · cited by 5,352
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- SMulCommClassstatement and proof · cited by 1,927
- FiniteDimensionalstatement and proof · cited by 1,854
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.