coe_mul — Mathlib

English

For f,g: α → M, the germ of their pointwise product equals the product of their germs: ↑(f * g) = (f * g : Germ l M).

Русский

Для функций f,g: α → M жерма их точечного произведения равна произведению жерм: ↑(f * g) = (f * g : Germ l M).

LaTeX

$$$ \\uparrow(f * g) = (f * g : \\mathrm{Germ}(l, M)) $$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul [Mul M] (f g : α → M) : ↑(f * g) = (f * g : Germ l M) :=
  rfl

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