instDivUniformOnFun — Mathlib

English

If β is a monoid, then a division operation is defined pointwise on UniformOnFun α β, i.e., UniformOnFun α β inherits a monoid structure with division defined componentwise.

Русский

Если β — моноид, то операция деления определяется покомпонентно на UniformOnFun α β, т.е. UniformOnFun α β наследует структуру моноида с делением покомпонентно.

LaTeX

$$$[Div\ β] \Rightarrow (UniformOnFun\ α\ β) \text{ has a pointwise division: } (f/g)(x)=f(x)/g(x)$$$

Lean4

@[to_additive]
instance [Div β] : Div (α →ᵤ[𝔖] β) :=
  Pi.instDiv

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