ofFun_div — Mathlib

English

If β is a division monoid, then ofFun preserves division: ofFun(f / g) = ofFun f / ofFun g.

Русский

Если β является дробленно-монодой, то отображение ofFun сохраняет деление: ofFun(f / g) = ofFun f / ofFun g.

LaTeX

$$$\operatorname{ofFun}(f / g) = \operatorname{ofFun} f / \operatorname{ofFun} g.$$$

Lean4

@[to_additive (attr := simp)]
theorem ofFun_div [Div β] (f g : α → β) : ofFun (f / g) = ofFun f / ofFun g :=
  rfl

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