pi_mem_of_mulSingle_mem — Mathlib

English

If for every i, the element Pi.mulSingle i (x_i) lies in H, then x ∈ H where H is a subgroup of the product ∀ i, f_i.

Русский

Если для каждого i элемент Pi.mulSingle i (x_i) лежит в H, тогда x ∈ H, где H — подгруппа произведения.

LaTeX

$$$\forall i,\, H(i) \ni Pi.mulSingle i (x_i) \Rightarrow x \in H$$$

Lean4

@[to_additive]
theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀ i, f i)} (x : ∀ i, f i)
    (h : ∀ i, Pi.mulSingle i (x i) ∈ H) : x ∈ H :=
  Submonoid.pi_mem_of_mulSingle_mem x h

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