English
For a finite index set η, if for each i in a finite set I the element Pi.mulSingle i (x_i) lies in H and for i not in I, x_i = 1, then the element x ∈ H.
Русский
Для конечного множества η, если для каждого i в конечном наборе I элемент Pi.mulSingle i (x_i) ∈ H, а для i ∉ I x_i = 1, тогда x ∈ H.
LaTeX
$$$\text{Given } I\subseteq η,\ x_i,\text{ if } (\forall i\in I,\ Pi.mulSingle i (x_i) \in H) \text{ and } (\forall i\notin I, x_i=1) \Rightarrow x\in H$$$
Lean4
@[to_additive (attr := deprecated Submonoid.pi_mem_of_mulSingle_mem_aux (since := "2025-10-08"))]
theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : Subgroup (∀ i, f i)} (x : ∀ i, f i)
(h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → Pi.mulSingle i (x i) ∈ H) : x ∈ H :=
Submonoid.pi_mem_of_mulSingle_mem_aux I x h1 h2
