coe_div — Mathlib

English

The germ extension preserves division of functions: for any f,g: α → M, where M has a division, the germ of the pointwise quotient f/g equals the quotient of the germs of f and g.

Русский

Пусть l — фильтр на α, M — множество с операцией деления. Для любых функций f,g: α → M верно: ↑(f/g) = ↑f / ↑g в Germ l M.

LaTeX

$$$ \\uparrow\\left(\\frac{f}{g}\\right) = \\left(\\frac{f}{g}\\right) \\;\\text{в } \\mathrm{Germ}(l,M). $$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_div [Div M] (f g : α → M) : ↑(f / g) = (f / g : Germ l M) :=
  rfl

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