99 ∃ P : ℝ → ℝ → ℝ, 100 (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧ 101 (∀ u v, P u v = P v u) ∧ 102 (∀ x y : ℝ, 0 < x → 0 < y → 103 m.cost (x * y) + m.cost (x / y) = P (m.cost x) (m.cost y)) 104 105/-! ## The Derivation Theorem -/ 106 107/-- **L4 is automatic in the polynomial form for any multiplicative recognizer.** 108 109The route-independence field of `SatisfiesLawsOfLogic` already provides the 110polynomial-degree-2 combiner satisfying the multiplicative L4. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.