pith. machine review for the scientific record. sign in
def definition def or abbrev

HasMultiplicativeConsistency

show as:
view Lean formalization →

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)

  72def HasMultiplicativeConsistency (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ) : Prop :=

proof body

Definition body.

  73  ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)
  74
  75/-! ## Derived Reciprocity (P-symmetry ⇒ F(x) = F(1/x)) -/
  76
  77/-- If the combiner `P` is symmetric and `F` is multiplicatively consistent with `P`,
  78then `F(x/y) = F(y/x)` for all `x,y>0`. -/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.