Theorems · Theorem · group theory

Submonoid.pi_mem_of_mulSingle_mem

∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] {S : Type u_3}
  [inst_1 : SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [Finite η] [inst_4 : DecidableEq η] {H : S}
  (x : (i : η) → f i), (∀ (i : η), Pi.mulSingle i (x i) ∈ H) → x ∈ H

Defined in

Mathlib.Algebra.Group.Submonoid.Finite

Cited by

2 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MulOneClassSetLikeSubmonoidClassFiniteDecidableEq