No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
115theorem Fquad_flat_ODE : SatisfiesFlatODE Gquad := Gquad_satisfies_flat
proof body
Term-mode proof.
116
117/-- The two ODEs are mutually exclusive. -/
depends on (5)
Lean names referenced from this declaration's body.
-
Gquad
in IndisputableMonolith.Foundation.DAlembert.Counterexamples
decl_use
-
Gquad
in IndisputableMonolith.Foundation.DAlembert.CurvatureGate
decl_use
-
Gquad_satisfies_flat
in IndisputableMonolith.Foundation.DAlembert.CurvatureGate
decl_use
-
SatisfiesFlatODE
in IndisputableMonolith.Foundation.DAlembert.CurvatureGate
decl_use
-
two
in IndisputableMonolith.QFT.SpinStatistics
decl_use