def definition def or abbrev

`modifiedPoissonStub`

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

formal statement (Lean)

 124noncomputable def modifiedPoissonStub : ModifiedPoissonPDEFacts where
 125  poisson_solution_unique := by

proof body

Definition body.

 126    intro ρ w Φ₁ Φ₂ h₁ h₂ r hr
 127    exact ⟨0, rfl⟩
 128  fundamental_modified_poisson := by
 129    intro ψ₀ ng ρ α C_lag x
 130    simp
 131
 132instance : ModifiedPoissonPDEFacts := modifiedPoissonStub
 133

depends on (1)

Lean names referenced from this declaration's body.

C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use