mulIndicator_comp_of_one — Mathlib

English

If g(1) = 1, then computing the indicator of the composition g ∘ f with respect to s equals composing g with the indicator of f on s.

Русский

Если g(1) = 1, то mulIndicator s (g ∘ f) = g ∘ mulIndicator s f.

LaTeX

$${g : M → N} (hg : g 1 = 1) : mulIndicator s (g ∘ f) = g ∘ mulIndicator s f$$

Lean4

@[to_additive]
theorem mulIndicator_comp_of_one {g : M → N} (hg : g 1 = 1) : mulIndicator s (g ∘ f) = g ∘ mulIndicator s f :=
  by
  funext
  simp only [mulIndicator]
  split_ifs <;> simp [*]

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