mulIndicator_div — Mathlib

English

For f,g: α → G, mulIndicator s (f/g) = mulIndicator s f / mulIndicator s g. The indicator respects division pointwise.

Русский

Индикатор сохраняет деление: mulIndicator s (f/g) = mulIndicator s f / mulIndicator s g.

LaTeX

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

Lean4

@[to_additive]
theorem mulIndicator_div (s : Set α) (f g : α → G) :
    (mulIndicator s fun a => f a / g a) = fun a => mulIndicator s f a / mulIndicator s g a :=
  (mulIndicatorHom G s).map_div f g

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