English
For any subset S of α and any monoid M with unit 1, the function sending x to 1_M when x ∈ S and also 1_M when x ∉ S is the constant-1 function. In particular, mulIndicator S (λ _ , 1) equals the constant function 1.
Русский
Пусть S ⊆ α и M обладает единицей 1. Функция, которая принимает значение 1_M независимо от x (то есть как на S, так и вне S), является константной функцией 1. Т.е. mulIndicator S (λ _, 1) = λ x, 1.
LaTeX
$$$ (\\mathrm{mulIndicator}(S, \\lambda x: M, 1)) = (\\lambda x: M, 1)$$$
Lean4
@[to_additive (attr := simp)]
theorem mulIndicator_one (s : Set α) : (mulIndicator s fun _ => (1 : M)) = fun _ => (1 : M) :=
mulIndicator_eq_one.2 <| by simp only [mulSupport_fun_one, empty_disjoint]
