mulIndicator_div' — Mathlib

English

For f,g: α → G, mulIndicator s (f / g) = mulIndicator s f / mulIndicator s g. A variant of the previous fact.

Русский

Утверждается то же самое для деления с индикатором.

LaTeX

$$$$ \\forall s:\\ Set\\,\\alpha, f,g:\\alpha \\to G,\\ mulIndicator s (f / g) = mulIndicator s f / mulIndicator s g $$$$

Lean4

@[to_additive]
theorem mulIndicator_div' (s : Set α) (f g : α → G) : mulIndicator s (f / g) = mulIndicator s f / mulIndicator s g :=
  mulIndicator_div s f g

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