mulIndicator_inv' — Mathlib

English

For a Group G, mulIndicator s f⁻¹ = (mulIndicator s f)⁻¹. The indicator commutes with taking inverses.

Русский

Для группы G индикатор сохраняет обратное: mulIndicator s f⁻¹ = (mulIndicator s f)⁻¹.

LaTeX

$$$$ \\forall s:\\ Set\\,\\alpha, f:\\alpha \\to G,\\quad mulIndicator s f^{-1} = (mulIndicator s f)^{-1} $$$$

Lean4

@[to_additive]
theorem mulIndicator_inv' (s : Set α) (f : α → G) : mulIndicator s f⁻¹ = (mulIndicator s f)⁻¹ :=
  (mulIndicatorHom G s).map_inv f

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