Theorems · Theorem · group theory

Submonoid.pi_le_iff

∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : (i : η) → Submonoid (f i)} {J : Submonoid ((i : η) → f i)},
  Submonoid.pi Set.univ H ≤ J ↔ ∀ (i : η), Submonoid.map (MonoidHom.mulSingle f i) (H i) ≤ J

For finite index types, the Submonoid.pi is generated by the embeddings of the monoids.

Defined in

Mathlib.Algebra.Group.Submonoid.Finite

Cited by

2 results in Mathlib

Foundations

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

Assumes

MulOneClassFiniteDecidableEq