toFun_mul — Mathlib

English

For f,g in α →ᵤ[𝔖] β, the product under toFun 𝔖 behaves pointwise: toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g.

Русский

Для f,g ∈ α →ᵤ[𝔖] β произведение под toFun 𝔖 действует по точкам: toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g.

LaTeX

$$$\forall f,g : \alpha \to^u_{\mathfrak{S}} \beta,\; \operatorname{toFun}_{\mathfrak{S}}(f * g) = \operatorname{toFun}_{\mathfrak{S}} f * \operatorname{toFun}_{\mathfrak{S}} g.$$$

Lean4

@[to_additive (attr := simp)]
theorem toFun_mul [Mul β] (f g : α →ᵤ[𝔖] β) : toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g :=
  rfl

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