def definition def or abbrev

`weakFieldAlgebraStub`

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

formal statement (Lean)

 103noncomputable def weakFieldAlgebraStub : WeakFieldAlgebraFacts where
 104  inverse_first_order_identity_minkowski := by

proof body

Definition body.

 105    intro h x μ ν
 106    have : |(0 : ℝ)| ≤ 8 * h.eps + 4 * h.eps ^ 2 := by
 107      have hnonneg : 0 ≤ 8 * h.eps + 4 * h.eps ^ 2 := by
 108        have := le_of_lt h.eps_pos
 109        nlinarith [this]
 110      simpa using hnonneg
 111    simpa using this
 112
 113instance : WeakFieldAlgebraFacts := weakFieldAlgebraStub
 114