mulIndicator_compl — Mathlib

English

A further variant of how mulIndicator interacts with division of functions; 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 indicator_compl']
theorem mulIndicator_compl (s : Set α) (f : α → G) : mulIndicator sᶜ f = f * (mulIndicator s f)⁻¹ :=
  eq_mul_inv_of_mul_eq <| s.mulIndicator_compl_mul_self f

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