def definition def or abbrev

`radialPoissonStub`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 134noncomputable def radialPoissonStub : RadialPoissonFacts where
 135  laplacian_spherical := by

proof body

Definition body.

 136    intro f r
 137    simp
 138  radial_poisson_solution_exists := by
 139    intro rho w
 140    exact ⟨fun _ => 0, by intro r hr; simp [RadialPoissonPhi]⟩
 141
 142instance : RadialPoissonFacts := radialPoissonStub
 143