toFun_div — Mathlib

English

For f,g ∈ α →ᵤ[𝔖] β with [Div β], toFun 𝔖 preserves division: toFun 𝔖 (f / g) = toFun 𝔖 f / toFun 𝔖 g.

Русский

Для f,g ∈ α →ᵤ[𝔖] β с [Div β], toFun 𝔖 сохраняет деление: toFun 𝔖 (f / g) = toFun 𝔖 f / toFun 𝔖 g.

LaTeX

$$$\operatorname{toFun}_{\mathfrak{S}}(f / g) = \operatorname{toFun}_{\mathfrak{S}} f / \operatorname{toFun}_{\mathfrak{S}} g.$$$

Lean4

@[to_additive (attr := simp)]
theorem toFun_div [Div β] (f g : α →ᵤ[𝔖] β) : toFun 𝔖 (f / g) = toFun 𝔖 f / toFun 𝔖 g :=
  rfl

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