seminormFromConst_def — Mathlib

English

If x is multiplicative for f, then seminormFromConst' hf1 hc hpm is multiplicative in x, i.e., for all y, seminormFromConst'(xy) = seminormFromConst'(x) · seminormFromConst'(y).

Русский

Если x мультипликативен для f, то seminormFromConst' hf1 hc hpm является мультипликативной по x: для всех y выполняется равенство.

LaTeX

$$∀ {x}, (∀ y, f(xy)=f x f y) → ∀ y, seminormFromConst'(xy) = seminormFromConst'(x) seminormFromConst'(y)$$

Lean4

theorem seminormFromConst_def (x : R) : seminormFromConst hf1 hc hpm x = seminormFromConst' hf1 hc hpm x :=
  rfl

Похожие утверждения